# Questions tagged [type-theory]

Type structure is a syntactic discipline for enforcing levels of abstraction.

57 questions
Filter by
Sorted by
Tagged with
1k views

### Can Elementary Affine Logic be used as the core type system of a practical programming language?

Elementary Affine Logic is a type system which captures the class of λ-terms that can be reduced in elementary time. Moreover, EAL-typeable terms can be reduced using the abstract fragment of Lamping'...
• 3,177
245 views

### How to encode a function from an existential type

I am having trouble using parametricity to show that existential types work in System F (or System Fω) in the way one would expect them to work. It is known that an existential type $\exists t.~P~t$ (...
• 552
4k views

### Classification of Typed/Untyped Lambda Calculi

Can anyone explain briefly (if thats possible!) or refer me to a reference, summarizing the differences between untyped lambda calculus and the more common typed lambda calculi? I'm particularly ...
• 293
1k views

### Can boolean algebra be expressed in simply typed lambda caclulus?

Boolean algebra can be expressed in untyped lambda calculus in (for example) this way. ...
2k views

### What exactly is "large elimination"?

I'm studying type theory (mostly Coq) and often encounter the term "large elimination", usually when talking about type universes hierarchy consistency, for example: impredicative polymorphism + ...
• 201
4k views

### How do 'tactics' work in proof assistants?

Question: How do 'tactics' work in proof assistants? They seem to be ways of specifying how to rewrite a term into an equivalent term (for some definition of 'equivalent'). Presumably there are formal ...
• 1,325
6k views

### Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
• 2,611
7k views

### What is the most intuitive dependent type theory I could learn?

I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
• 1,325
5k views

### How would I go about learning the underlying theory of the Coq proof assistant?

I'm going over the course notes at CIS 500: Software Foundations and the exercises are a lot of fun. I'm only at the third exercise set but I would like to know more about what's happening when I use ...
3k views

### Type classes vs object interfaces

I don't think I understand type classes. I'd read somewhere that thinking of type classes as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem ...
• 463
2k views

### Why naturals instead of integers?

I'm interested in why natural numbers are so beloved by the authors of books on programming languages theory and type theory (e.g. J. Mitchell, Foundations for programming languages and B. Pierce, ...
• 1,103
1k views

### Are types propositions? (What are types exactly?)

I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in ...
2k views

### Context Sensitive Grammars and Types

1) What, if any, is the relationship between static typing and formal grammars? 2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
3k views

### Why do Agda and Coq disagree on strict positivity?

I've stumbled across a confusing disagreement between Agda and Coq that is not obviously related to the most well known distinctions between their type theories (e.g., (im)predicativity, induction-...
• 471
2k views

### Why it's impossible to declare an induction principle for Church numerals

Imagine, we defined natural numbers in dependently typed lambda calculus as Church numerals. They might be defined in the following way: ...
• 1,762
3k views

### Is there a typed lambda calculus which is consistent and Turing complete?

Is there a typed lambda calculus where the corresponding logic under the Curry-Howard correspondence is consistent, and where there are typeable lambda expressions for every computable function? This ...
2k views

### Implicit vs explicit subtyping

This page asserts that many languages do not use implicit subtyping (structural equivalence), prefering explicit/declared subtyping (declaration equivalence) I've mostly used programming ...
586 views

### Minimal specification of Martin-Löf type theory

I'm reading the formal presentation of Martin-Löfs type theory (appendix of the HoTT book). The authors introduce a hierarchy of universes, then $\Pi, \Sigma,+, {\bf 0}, {\bf 1}$ and also $W$-types as ...
• 505
1k views

### Can we prove weak normalization for System F by induction on a transfinite ordinal

Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
805 views

### Relative consistency of PA and some type theories

For a type theory, by consistency, I mean that it has a type which is not inhabited. From the strong normalization of the lambda cube, it follows that system $F$ and system $F_\omega$ are consistent. ...
• 343
615 views

### Logical Reations for an Impredicative System in a Predicative MetaTheory

Logical Relations for Impredicative languages like System F seem to rely critically on impredicativity of the ambient logic. Specifically, the interpretation for the forall-type will be defined in ...
• 1,695
1k views

• 145
220 views

### Type of induction principle for fixpoint types

To the Calculus of Constructions we could add a general fixpoint type constructor (accepting inconsistencies or assuming F is a ...
• 701