36
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ The HoTT book has an introduction which compares types and sets, perhaps that will help, see Section 1.1 of homotopytypetheory.org/book . But more importantly, you want us to implant in your head directly the correct idea of types, whereas for sets you're happy to have them described by axioms, without insisting to know "what they really are". Well, types are described by the inference rules for types. And they have a very intuitive concrete model, you know, a basked filled with Lego blocks. Whatever you can build from them is in the type. $\endgroup$ – Andrej Bauer Sep 30 '13 at 0:31
  • $\begingroup$ I think getting my brain away from set theory is the biggest issue. However, I'm not sure how good the Lego analogy is. What are the blocks? If x:A and y:A typically I can't build anything from them unless A is some recursive arrow type. Of course I can often mix stuff of different type to build something of a third type... $\endgroup$ – dst Sep 30 '13 at 7:39
  • 4
    $\begingroup$ The Lego blocks are the type constructors. So for instance from $x : A$ and $y : A$ you can build $(x,y)$ and $(x,x)$ and $\mathsf{inl}(x)$, and $\mathsf{relf}_x$ and $\lambda z : A . x$. You can also build new types, for instance $\mathsf{Id}(x,y)$ and $\sum_{z : A} \mathsf{Id}(x,z)$, and so on. People have different intuitions about types. Sets is one of them, but crude. Types are also like topological spaces. They are also like structured data in programming. They are also like $\omega$-groupoids. That's the beauty of it, the richness of possibilities. Pick one possiblity and run with it. $\endgroup$ – Andrej Bauer Sep 30 '13 at 8:08
31
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ +1 for TAPL. I was able to teach myself quite a bit about types from reading that book. $\endgroup$ – Guy Coder Sep 30 '13 at 17:14
  • $\begingroup$ I'm not sure ATTAPL is a good starting point to learn about dependent types. $\endgroup$ – Martin Berger Oct 1 '13 at 12:48
15
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ This was extremely useful. I think one major issue of anyone coming into constructive mathematics is to unlearn a lot of things. $\endgroup$ – dst Oct 2 '13 at 19:51
  • $\begingroup$ I agree. It takes a while to unlearn one's unacknowledged set-theoretic assumptions. Doing a lot of Agda programming helped me, and might work for you too if you come from a computer science background. $\endgroup$ – Martin Berger Oct 2 '13 at 20:56
10
$\begingroup$

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

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.

$\endgroup$
  • $\begingroup$ I actually know Haskell. My problem is that any tutorial will just tell you how to define types, but never what they actually are. It just seems to be some magic tag attached to all your data, so that the type checker can pick the right version of a polymorphic function and check that things are not mixed in ways that don't make sense. They still leave the question open of what a type is. I'm especially puzzled by this, since Voevodsky & co is trying to base all of math on this, yet, I've never seen a precise definition. $\endgroup$ – dst Sep 29 '13 at 19:42
  • 2
    $\begingroup$ In Haskell you have typing judgements $\Gamma \vdash M : \alpha$ where $M$ is a program, $\alpha$ is the type of $M$, assuming that $M$'s free variables are typed as assumed in the typing environment $\Gamma$. In first approximation, Haskell types themselves are 'blobs', syntactic markers. That's exactly the same in Martin-Löf type theory. It just happens to be the case that the types, the 'blobs', the syntactic markers of Martin-Löf type theory are more complicated than those of Haskell. $\endgroup$ – Martin Berger Sep 29 '13 at 20:39
  • $\begingroup$ Types are very precisely defined in Haskell, in Martin-Löf type theory and in Voevodsky's homotopy type theory. There is no ambiguity whatsoever. For example Appendix A.2 gives a proof-system for all terms and types of homotopy type theory. If you want even more rigour, you can look at the Coq or Agda formalisations. $\endgroup$ – Martin Berger Sep 29 '13 at 20:42
  • 2
    $\begingroup$ Maybe you need to swallow that types have no essence other than how they are defined. This is not different with e.g. Sets, they are given by the axioms of set theory. (This is not quite true, but it is nevertheless important to understand.) $\endgroup$ – Martin Berger Sep 29 '13 at 20:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.