Questions tagged [type-theory]

formal systems to specify properties of objects

Filter by
Sorted by
Tagged with
0
votes
1answer
36 views

What are the difference and relation between type checking and type reconstruction?

In Types and Programming Languages by Pierce, ML-style let-polymorphism was first described by Milner (1978). A num- ber of type reconstruction algorithms have been proposed, notably the clas- ...
-1
votes
1answer
85 views

What is “Hindley-Milner (i.e., unification-based) polymorphism”?

In Types and Programming Languages by Pierce, Ch11 Simple Extensions extends the typed lambda calculus. Section 11.5 Let Bindings says: In Chapter 22 we will see another reason not to treat let as ...
3
votes
0answers
74 views

Does Hindley-Milner refer to the unification algorithm for type reconstruction, a type system, or a form of polymorphism?

What does Hindely-Milner refer to? In Types and Programming Languages by Pierce, I only find that Section 22.4 Unification mentions "Hindley" and "Milner", when introducing the unification algorithm. ...
1
vote
1answer
85 views

Types and Programming Languages - proof for theorem about principles of induction of terms

Types and Programming Languages book introduces a theorem about principles of induction on term (p. 31, theorem 3.3.4): Suppose P is a predicate on terms. Induction on depth: If, for each ...
0
votes
1answer
35 views

What does valid method overriding mean?

In Types and Programming Languages by Pierce, from p257 to p258, about featherweight Java, The predicate override(m, D, C→C0) judges whether a method ...
1
vote
2answers
77 views

Which is a type of objects in mainstream OO languages: a class, an interface, an abstract class, a metaclass?

In Types and Programming Languages by Pierce, Section 18.6 Simple Classes in Chapter 18 Imperative Objects says: We should emphasize that these classes are values, not types. Also we can, if we ...
10
votes
1answer
1k views

Why does Coq include let-expressions in its core language

Coq includes let-expressions in its core language. We can translate let-expressions to applications like this: let x : t = v in b ~> (\(x:t). b) v I understand ...
1
vote
1answer
82 views

Does an ADT have multiple or only one representations/implementations?

Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types: A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
0
votes
1answer
32 views

Why can System F1 a.k.a. λ → have kind `*`, but no quantification `∀`?

In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of 30.4.1 Definition: In System F1 , the only kind is ...
-1
votes
1answer
79 views

What order logic does a system correspond to under Curry–Howard correspondence?

In Types and Programming Languages by Pierce, Section 9.4 Curry–Howard correspondence on p109 has a table Does the table mean that the simply typed lambda calculus ...
1
vote
1answer
52 views

Is `→` a type operator?

In Types and Programming Languages by Pierce, The level of types contains two sorts of expressions. First, there are proper types like Nat, Nat→Nat, Pair Nat Bool, and ∀X.X→X, which are ...
0
votes
0answers
56 views

Is the language “untyped arithmetic expressions” in Types and Programming Languages not Turing complete?

In Types and Programming Languages by Pierce, is it correct that the language introduced in Chapter 3 Untyped Arithmetic Expressions is not Turing complete? Because it doesn't provide recursion. the ...
1
vote
1answer
47 views

What are the differences and relations between a type constructor and a type operator?

What are the definitions of a type constructor and a type operator? What are their differences and relations? I think a type operator is a function whose parameters are n types and return is a type. A ...
1
vote
2answers
186 views

How can an existential type be defined in terms of universal type?

In Types and Programming Languages by Pierce, how does the following achieve the definition of an existential type in terms of universal type, by polymorphic version of Church encoding of pairs? ...
0
votes
1answer
65 views

Why are ADT packages opened immediately after they are built, while existential objects opened as late as possible?

Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types: A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
0
votes
1answer
89 views

How can mainstream OO languages support strong binary operations by classes?

Section 24.2 in Types and Programming Languages by Pierce compares ADT and existential objects,in terms of how well they support strong binary operations: Other binary operations cannot be ...
0
votes
1answer
48 views

Are type abstraction values and universal types not for non functions, but only for functions?

In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types". ...
0
votes
1answer
40 views

How does this allow list operations to be applied to lists with elements of any type?

In Types and Programming Languages by Pierce, Chapter 11 is simple extensions of the simply typed lambda calculus with any simple base types. Section 11.12 introduces Lists. How does the section ...
0
votes
1answer
31 views

What is the purpose of erasing a type application to a term-application in parametric polymorphism?

From Types and Programming Languages by Pierce 23 Polymorphism 23.7 Erasure and Evaluation Order in a full-blown programming language, which may include side- effecting features such as ...
0
votes
1answer
54 views

Does a term being normalizable mean the same as the term has a normal form?

From Types and Programming Languages by Pierce A term $t$ is in normal form if no evaluation rule applies to it— i.e., if there is no $t'$ such that $t -→ t'$. and A term $t$ is typable (or ...
0
votes
1answer
84 views

Do the following concepts belong to syntax or semantics?

I am not very sure about the difference between syntax and semantics. Does each of the following concepts belong to syntax or semantics? terms values: terms that are possible final results of ...
1
vote
1answer
60 views

Do determinacy of one-step evaluation and uniqueness of normal forms apply to all (or most) languages in TAPL?

In Types and Programming Languages by Pierce, when talking about untyped arithmetic expressions in Chapter 3, there are two theorems: $-→$ is single-step evaluation relation: 3.5.4 Theorem [...
1
vote
1answer
42 views

Does Types and Programming Languages use a recursive equation to define a recursive type or its generator?

In Types and Programming Languages by Pierce et al: The recursive equation specifying the type of lists of numbers is similar to the equation specifying the recursive factorial function on page 52: ...
0
votes
0answers
35 views

General term for upcasting and downcasting?

Is there a more precise term than simply "casting"? "Casting" often includes for example integer -> float or ...
3
votes
0answers
74 views

Calculus of constructions, type-in-type and recursion

Does adding type-in-type to the calculus of constructions lead to (general) recursion? Such that one can write the Y combinator.
0
votes
0answers
35 views

How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?

I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
0
votes
1answer
61 views

Could following be a counter example to Church-Rosser (Confluence) theorem?

According to the "Type Theory and Formal Proof" book, Church-Rosser theorem (confluence) is as follow: Suppose that for a given term $M$, we have $M \twoheadrightarrow_\beta N_1$ and $M\...
6
votes
1answer
336 views

What does canonicity property mean in Type Theory?

The "Computational Component" section of the Type Theory - Wikipedia (as well as a few papers about cubical type theory and 2d type theory) talk about canonicity property. Would you please explain ...
2
votes
1answer
100 views

Difference between computation in proposition proof and definitional computation?

As stated in equality at nLab, "computational equality" is about computational steps which take for example, $s(s(0))+ s(0)$ to $s(s(s(0)))$ and it acts exactly and can be considered same as ...
4
votes
2answers
104 views

Why values can not be replaced with their extensionally equal values in an intensional system?

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that: Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the ...
3
votes
1answer
126 views

Definition of extensional and propositional equality in Martin-Lof extensional type theory

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.[4-5]) that: A similar situation occurs in extensional Martin-Lof type theory where propositional and definitional ...
4
votes
1answer
217 views

Definitional equality of two propositions about propositional equality

Martin Hofmann states in Extensional Concepts in Intensional Type Theory (§1.1 p.3) that: It is important that definition equality is pervasive so if M and N are definitionally equal then P(M) is ...
8
votes
1answer
523 views

Representation of the concatenation at the type level

I would like to learn more about concatenative programming through the creation of a small simple language, based on the stack and following the concatenative paradigm. Unfortunately, I haven't found ...
2
votes
0answers
41 views

Real world example of contraction and weakening

Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t ...
0
votes
1answer
69 views

Subtyping and subkinding, are they relevant?

I'm thinking about a type system that has some special kind of some certain types that are subtypes of the universe kind type. Imagine the typing relation, where $...
5
votes
1answer
74 views

What untyped term inhabits induction on natural numbers in CoC?

Induction on Church-encoded natural numbers (which I will call indNat) can not be defined within the Calculus of Constructions. If we assumed ...
0
votes
1answer
43 views

How does this example violate Liskov substitution principle, which then causes violation of the open-closed principle?

From Agile Principles, Patterns, and Practices in C# by Robert Martin, Listing 10-1. A violation of LSP causing a violation of OCP ...
2
votes
2answers
171 views

Type theory for imperative programming languages?

The type theory that I have seen is all developed over lambda calculus, which is an inherently functional language. Nevertheless, in practice imperative languages have type systems. Are there ...
28
votes
4answers
4k views

What's the difference between a type and a kind?

I am learning the programming langauge Haskell, and I'm trying to wrap my head around what the difference between a type and a ...
2
votes
0answers
153 views

Proving that the failure of algorithm W implies that the program is not typable

How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ? The original paper ...
3
votes
0answers
33 views

Is the expression (λx.xx)(λy.y) typeable in the following system?

We are given a simple functional language: $ e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$ with types: $\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2} $ Is the ...
2
votes
0answers
36 views

Substituting a term for a variable in a context

At this link you can read Nicola Gambino's slides on one way to approach the formal syntax of Martin-Löf dependent type theory. (They are concise and very readable.) On slide 10, he gives a standard ...
2
votes
3answers
89 views

How is functional property guaranteed in type theory when function type is defined?

I understand that functions are not defined in type theory the same way they are defined in set theory, hence functional property is not directly defined when defining function type in type theory. ...
1
vote
0answers
95 views

Is it possible to write a fully-decidable type system for the J language?

I'm experimenting with the J array language, a dynamically-typed array language with mutable assignment, subtyping, and function overloading (just like traditional APL). It is unclear to me whether ...
1
vote
0answers
41 views

Design considerations of datatypes in early programming languages like C

Although type theory originated (e.g. already discussed by Russell in 1910s) much earlier than programming languages, I have this feeling that languages such as C considered type-checking from a very ...
0
votes
1answer
71 views

Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming ...
12
votes
5answers
1k views

Is there any use case for the bottom type as a function parameter type?

If a function has return type of ⊥ (bottom type), that means it never returns. It can for example exit or throw, both fairly ordinary situations. Presumably if a function had a parameter of type ⊥ it ...
6
votes
1answer
81 views

Reversing an application of `sym` to `ua` and `isoToEquiv` in cubical type theory

I am proving a kind of structure invariance principle for magmas in Cubical Type Theory with the Agda/Cubical library. This is done by constructing a path between two simple magmas and then ...
6
votes
1answer
118 views

Can all regular tree types be expressed as $\mu$ types?

In "Types and Programming Languages", Pierce gives a translation from recursive types ($\mu$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct ...
2
votes
1answer
91 views

Relationship between dependent sum type and dependent product type?

Since dependent sum type ($\sum_{n\in \mathbb{N}} P(n) $) is interpreted as ($\exists n\in \mathbb{N}:P(n) $) and dependent product type ($\prod_{n\in \mathbb{N}} P(n)$) is interpreted as ($\forall n\...

1 2
3
4 5
10