# Questions tagged [type-theory]

formal systems to specify properties of objects

412 questions
Filter by
Sorted by
Tagged with
15 views

### Is possible to construct a fixed set of typeclases as powerful as unconstrainde typeclasses?

We can construct a fixed set of combinators with a computational power equivalent to lambda calculus. Can we do the same with typeclasses (ad-hoc polymorphism)? For example, construct a finite set ...
54 views

### Why is the type ∀t.t un-inhabited in System F?

How do you prove that there exists no term with the type $\forall t. t$ in System F? I tried searching through Pierce's TAPL and Reynold's ToPL, but could not find anything. I suspect that the proof ...
1k views

### What do the ∀ and ∃ symbols mean in the Axiom of Choice?

On the Wikipedia page for the Axiom of Choice the following statement is given: $(\forall x^\sigma)(\exists y^\tau)R(x,y)\rightarrow(\exists f^{\sigma \rightarrow \tau})(\forall x^\sigma)R(x, f(x))$ ...
37 views

### What is the difference between a Type and an Abstract Type?

In my data structures course we are given definitions for Type and Abstract Type but they confuse me. A type is a set of values and the operations you can do on them. The set of operations is ...
35 views

### in the lambda calculus with products and sums is $f : [n] \to [n]$ $\beta\eta$ equivalent to $f^{n!}$?

$\eta$-reduction is often described as arising from the desire for functions which are point-wise equal to be syntactically equal. In a simply typed calculus with products it is sufficient, but when ...
44 views

30 views

### On the diamond property for $F_{\omega}$ in TAPL

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction: $S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$ ...
54 views

### Are the permutation or weakening lemmas needed for term substitution?

In TAPL book, page 453, Pierce discusses the following lemma: $\Gamma , x:S , \Delta \vdash t:T \land \Gamma \vdash s:S \implies \Gamma, \Delta \vdash [x \mapsto s]t:T$ He claims that when $t$ is ...
23 views

### What the type of an overloaded function should be?

Anecdotally, Virgill III language forbids overloading since overloading resolution is at odds with the language support of functions as first-class citizen, when resolution can't happen at compile ...
41 views

### Derivation of product type eliminator in type theory

In HoTT book, section 1.5 (Product Types) in order to define the eliminators for the product type it assumes a function of type $g:A \rightarrow B \rightarrow C$ and then goes on to define the ...
55 views

### How could 'Complete and Easy Bidirectional Type Checking' handle invariant parameters on type constructors

The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking ...
241 views

### Are “logarithm types” a thing?

I'm attempting to formalize some thoughts I've had about paths into data structures. For example, a path into a list of Ts might be a pair of an index with a path ...
41 views

### Simulating extensible sums with dependent types?

ML-style languages have a concept of "extensible" or "open" sum types, where variants can be declared at any point, and there's not a fixed number of constructors for the type. They're usually used to ...
41 views

### Rules for consistency with mutual inductive families?

I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other: ...
109 views

### Is this statement of P = NP in Agda correct?

Looking for a self-contained statement of P = NP in type theory, I stumbled upon this short Agda formalization (a cleaned up version is reproduced below). The statement here does seem to express the ...
36 views

### How is substitution in type theory the composition of classifying morphisms in category theory?

In the article at nlab about relation between category theory and type theory, it is said that substitution in type theory is the same as composition of classifying morphisms in category theory. ...
25 views

### Is, beta reduction in type theory being considered as counit for hom-tensor adjunction in category theory, a denotational or operational semantic?

In the article at nlab about the relation between type theory and category theory, it is said that "beta reduction" in type theory corresponds to "counit for hom-tensor adjunction" in category theory ...
76 views

### What is the language feature which allows a variable to be associated with values of different types?

In Python, I can change the types of values associated with a variable: >>> x=1 >>> x="abc" In C, I can't do the same. What is the name of ...
47 views

### Is the choice of static and dynamic typing not visible to the programmers of the languages? [closed]

From Design Concepts in Programming Languages by Turbak Although some dynamically typed languages have simple type markers (e.g., Perl variable names begin with a character that indicates the type ...
42 views

### Are type variables really only used in mathematical conversation about types?

Are type variables really only used in mathematical conversation about types? i.e. are type variables (meta-variables that only contain the type classification label) only exist in proofs for types ...
87 views

### What is the difference between $\alpha \to \alpha$ vs $\forall \alpha. \alpha \to \alpha$?

I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a ...
80 views

### What does $\forall \alpha_1, \dots , \alpha_n . \tau$ mean formally as a type?

I was learning about polymorphic types but I couldn't understand the notation, can someone explain it means (context cs421 UIUC): $$\forall \alpha_1, \dots , \alpha_n . \tau$$ its supposed to be a ...
43 views

### How do you define and parse variables (free or bound) from user-entered strings?

I'm writing an application in which the user might enter expressions such as $\text{lim}_{i \in I} \beta(i)$ where $\beta$ is a functor. That's just an example, the expressions, which contain ...
57 views

### How is β-reduction a 2-morphism in Category theory?

According to Categorifying CCCs: Computation as a Process, computation or β-reduction process in untyped-lambda calculus is in fact a 2-morphism in category theory. Can someone please describe me ...
25 views

### Do Rank-1 (prenex) polymorphism and Predicative polymorphism mean the same?

https://en.wikipedia.org/wiki/Parametric_polymorphism says: Rank-1 (prenex) polymorphism In a prenex polymorphic system, type variables may not be instantiated with polymorphic types.[4] ...
27 views

### What are the relation and differences between reification and type passing semantics?

https://en.wikipedia.org/wiki/Type_erasure says type erasure refers to the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. ...
21 views

### What are the relations between these two descriptions of let polymorphism?

In Types and Programming Languages by Pierce, there are two descriptions of let-polymorphism. Sec23.8 Fragments of SystemF on p359 says This has led to various proposals for restricted fragments ...
30 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 ﬁrst described by Milner (1978). A num- ber of type reconstruction algorithms have been proposed, notably the clas- ...
49 views

### What is “Hindley-Milner (i.e., uniﬁcation-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 ...
22 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. ...
24 views

### Is it possible to deduce type from the lambda form?

I was continuing the exploration of lambda world this summer. When I take a look at the simply typed lambda calculus, it looks like there is no use for usual chuch numerals and boolean forms anymore. ...
50 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 ...
27 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 ...
56 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 ...
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 ...
34 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 ...
20 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 Deﬁnition: In System F1 , the only kind is ...
48 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 ...
10 views

### Can two type expressions in different kinds have subtyping relation and equivalence relation?

In Higher-order bounded quantiﬁcation ($F^ω_{<:}$), introduced in Ch31 in Types and Programming Langauges by Pierce, its subtyping and equivalence rules are: Does subtyping relation only exist ...
35 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 ...
25 views

### Does λ→ have type operators?

In Types and Programming Languages by Pierce, Ch11 Simple Extensions introduces λ→ as the simply typed lambda calculus with simple extensions, and introduces <...
26 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 ...
16 views

### How can we directly reaching inside and looking at the state of a partially existential object?

Types and Programming Languages by Pierce says in Section 26.5 Bounded Existential Types, about partial existential objects implemented in terms of bounded existential types: We can make a similar ...
26 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 ...
57 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? ...
60 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 ...