Intro to Martin-Löf type theory

Question

What would be the best introduction to Per Martin-Löfs ideas about type theory? I've looked at some lectures from the Oregon PL summer school, but I'm still sort of puzzled by the following question:

What is a type?

I know what a set is, since you can define them by the usual ZF axioms and they have a very intuitive concrete model; just think of a basket filled with stuff. However, I've yet to see a reasonable definition of a type and I was wondering if there is some source that would distill this idea for dummy.

Answer 1

A type is a property of computations. It's what you write on the right-hand side of a colon.

Let me elaborate on that. Note that the terminology isn't completely standard: some articles or books may use different words for certain concepts.

A term is an element of an abstract syntax that is intended to represent computation. Intuitively, it's a parse tree. Formally, it's a finite tree where the nodes belong to some alphabet. An untyped calculus defines a syntax for terms. For example, the (untyped) lambda calculus contains terms (written $M$, $N$, etc.) built from three types of nodes:

• variables, of arity 0 (a denumerable collection thereof), written $x$, $y$, etc.;
• application of a variable, of arity 1 (a denumerable collection thereof, with a bijection to variables), written $\lambda x. M$, etc.;
• application, of arity 2, written $M \, N$.

A term is a syntactic construction. A semantics relates terms to computations. There are many types of semantics, the most common being operational (describing how terms can be transformed into other terms) or denotational (describing terms by a transformation into another space, usually built from set theory).

A type is a property of terms. A type system for an untyped calculus describes which terms have which types. Mathematically, at the core, a type system is a relation between terms and types. More accurately, a type system is a family of such relations, indexed by contexts — typically, a context provides at least types for variables (i.e. a context is a partial function from variables to types), such that a term may only have a type in contexts that provide a type for all its free variables. What kind of mathematical object a type is depends on the type system.

Some type systems are described with types as sets, using notions of set theory such as intersection, union and comprehension. This has the advantage of resting upon familiar mathematical foundations. A limitation of this approach is that it doesn't allow reasoning about equivalent types.

Many type systems describe types themselves as terms in a calculus of types. Depending on the type system, these may be the same terms or different terms. I'll use the phrase base term to refer to a term of the calculus that describes computation. For example, the simply typed lambda calculus uses the following calculus of types (written $\tau$, etc.):

• base types, of arity 0 (a finite or denumerable collection thereof), written $A$, $B$, etc.;
• function, of arity 2, written $\tau_0 \rightarrow \tau_1$.

The relation between terms and types that defines the simply typed lambda calculus is usually defined by typing rules. Typing rules are not the only way to define a type system, but they are common. They work well for compositional type systems, i.e. type systems where the type(s) of a term is built from the types of subterms. Typing rules define a type system inductively: each typing rule is an axiom that states that for any instantiation of the formulas above the horizontal rule, the formula below the rule is also true. See How to read typing rules? for more details. Does there exist a Turing complete typed lambda calculus? may also be of interest.

For the simply typed lambda calculus, the typing judgement $\Gamma \vdash M : \tau$ means that $M$ has the type $\tau$ in the context $\Gamma$. I've omitted the formal definition of contexts. $$ \dfrac{x:\tau \in \Gamma}{\Gamma \vdash x : \tau}(\Gamma) \qquad \dfrac{\Gamma, x:\tau_0 \vdash M : \tau_1}{\Gamma \vdash \lambda x.M : \tau_0 \rightarrow \tau_1}(\mathord{\rightarrow}I) \qquad \dfrac{\Gamma \vdash M : \tau_0 \rightarrow \tau_1 \quad \Gamma \vdash N : \tau_0}{\Gamma \vdash M\,N : \tau_1}(\mathord{\rightarrow}E) $$

For example, if $A$ and $B$ are based types, then $\lambda x. \lambda y. x\,y$ has the type $(A \rightarrow B) \rightarrow A \rightarrow B$ in any context (from bottom to top, apply $(\mathord{\rightarrow}I)$ twice, then $(\mathord{\rightarrow}E)$, and finally $(\Gamma)$ on each branch).

It is possible to interpret the types of the simply typed lambda calculus as sets. This amounts to giving a denotational semantics for the types. A good denotational semantics for the base terms would assign to each base term a member of the denotation of all of its types.

Intuitionistic type theory (also known as Martin-Löf type theory) is more complex that simply typed lambda calculus, as it has many more elements in the calculus of types (and also adds a few constants to the base terms). But the core principles are the same. An important feature of Martin-Löf type theory is that types can contain base terms (they are dependent types): the universe of base terms and the universe of types are the same, though they can be distinguished by simple syntactic rules (usually known as sorting, i.e. assigning sorts to terms, in rewriting theory).

There are type systems that go further and completely mix types and base terms, so that there is no distinction between the two. Such type systems are said to be higher-order. In such calculi, types have types — a type can appear on the left-hand side of the $:$. The calculus of construction is the paradigm of higher-order dependent types. The lambda cube (also known as Barendregt cube) classifies type systems in terms of whether they allow terms to depend on types (polymorphism — some base terms contain types as subterms), types to depend on terms (dependent types), or types to depend on types (type operators — the calculus of types has a notion of computation).

Most type systems have been given set-theoretical semantics, to tie them with the usual foundations of mathematics. How are programming languages and foundations of mathematics related? and What is the difference between the semantic and syntactic views of function types? may be of interest here. There has also been work on using type theory as a foundation of mathematics — set theory is the historic foundation, but it is not the only possible choice. Homotopy type theory is an important milestone in this direction: it describes the semantics of intentional intuitionistic type theory in terms of homotopy theory and constructs set theory in this framework.

I recommend Benjamin Pierce's books Types and Programming Languages and Advances Topics in Types and Programming Languages. They are accessible to any undergraduate with no prerequisite other than basic familiarity with formal mathematical reasoning. TAPL describes many type systems; dependent types are the subject of chapter 2 of ATTAPL.

Answer 2

Maybe a better question for somebody coming from set theory and grappling with how set theory and Martin-Löf type theory differ, is to reflect on what sets are. Your intuitions about set theory and the foundations of mathematics will be infected with unquestioned set-theoretic assumptions that you take for granted. Alas Martin-Löf type theory does not share these assumptions.

Contrary to conventional understanding, set theory is a theory of two relations: equality and set membership, not just set membership. And these two relations are built in substantially distinct phases.

1. We build up first-order logic as a theory of equality of arbitrary things (not just sets). First-order logic uses an informal notion of proof. The concept proof is not itself expressible formally in first-order logic alone.

2. Then we build up set-theory on top of first-order logic as a theory of sets and set membership.

3. Set membership and equality are then related by the axiom of extensionality which says that two sets are equal exactly when they have the same members.

4. Finally, the informal concept of proof from (1) gets an ex-post rationalisation as certain sets (proof trees).

It is important thing to realise is that the notion of proof is thus a second-class citizen in set theory.

This set-up works fine for conventional small/medium sized mathematics, but as we are now tackling large-scale proofs, such as the classification of all finite simple groups, or the verification of non-trivial computer programs, it falls apart, because it does not lead itself to easy mechanisation.

Martin-Löf type theory is different: it builds up the notion of proof and that of type (which, roughly, is to Martin-Löf type theory what sets are to set theory) in one-fell swoop. This means proofs are first-class citizens of the theory. While a set is given by it's members, set theory omits to specify formally what counts as a proof that something is a set member. In contrast a type is given by its proofs of inhabitation. So you understand a type $T$ exactly when you understand what counts as a proof of $T$.

What are these proofs that inhabit types? Simplifying a bit (and omitting identity types), they are functional programs, more precisely terms in the $\lambda$-calculus that are typable. This is known as the Curry-Howard correspondence. It gives a beautiful new and less ad-hoc foundation of constructive mathematics. It doesn't work quite so well for classical mathematics tough.

Answer 3

I'm not aware of easy pathways into Martin-Löf type theory. I guess the following could serve as introductions.

• B. Nordström, K. Petersson, J. M. Smith, Martin-Löf's Type Theory.
• B. Nordström, K. Petersson, J. M. Smith, Programming in Martin-Löf's Type Theory.

However, if you are puzzled by the question "what is a type", I suggest to get into much simpler type-theories first. Any typed programming language will do, but e.g. Ocaml, F# and Haskell would be especially useful. Simplifying a bit, one could say that Martin-Löf type theory extends the types behind the aforementioned languages in two ways:

1. With dependent types. You find them in tamer form in various programming languages.
2. With identity types. This is the main innovation of Martin-Löf's over previous dependent type theories.

The key idea behind dependent types is simple: types can be parameterised by programs. This is not possible (simplifying a bit) in more conventional typing systems such as those mentioned above. While simple, the consequences are profound: dependent types lift the Curry-Howard correspondence to first-order constructive logic. Identity types are a bit unusual. If/when you are comfortable with a language like Haskell, you could learn Agda, which is basically Haskell with Martin-Löf type theory. I feel that Agda is much easier to learn for a programmer than reading the books mentioned above.