Bartosz Milewski: A Taste of Type Theory

I want to give programmers a taste of type theory and its connections to the foundations of mathematics. The destination is identity types: a way to express equality inside the theory. To get there, I first introduce recursion, dependent types, induction and propositions as types.

Consider the informal equation 1 × A = A. In programming terms, the unit type has one value, and pairing that value with an element of A adds no information. We can write a function that removes the unit and another that puts it back.

Strictly speaking, those functions suggest an isomorphism, not automatic equality: we still need to show they are inverses. In an ordinary programming language, an A and a pair of unit and A cannot necessarily be substituted for each other without conversion.

I introduce natural numbers with two constructors: zero and successor. Zero can be constructed directly; successor takes a natural number and constructs another. Repeated application gives zero, one, two and so on.

A type also needs an elimination rule: how can we define a function that consumes a natural number? Give a base value for zero and a step describing how to obtain the next result from the previous one. Together they define a recursive function.

A computation rule specifies how the resulting function behaves at zero and successor. Factorial provides an example: start with 1 and use a step that multiplies the previous result by the next number. The step itself need not be written as a recursive function.

A length-indexed vector illustrates a dependent type. Instead of one undifferentiated vector type, there is a family indexed by a natural-number length. An empty vector has length zero; adding an element to a vector of length n produces one of length n+1.

The result type depends on the value n. This lets the type checker track size relationships, so operations with incompatible lengths can be rejected according to the type rules. That differs from a type depending only on another type, such as a list of integers.

Now define a dependent function on natural numbers: for each n it returns a value whose type depends on n. A base constructs an empty vector; a step takes a length-n vector and adds a chosen element, producing a vector of length n+1. Repeating that step builds a vector filled with the element.

This dependent eliminator is called induction. Compared with ordinary recursion, the result type can change with the input. The computation rules still specify the behavior at zero and successor.

The propositions-as-types or Curry–Howard correspondence connects this construction to proof. A proposition is represented by a type, and a value inhabiting that type serves as a proof. For example, a proof of A and B corresponds to a pair containing a proof of A and a proof of B.

A family C(n) can represent a proposition for each natural number. The base is a proof of C(0), and the step transforms a proof of C(n) into a proof of C(n+1). The dependent eliminator therefore corresponds to mathematical induction.

An identity type expresses a proposition that two values x and y of a type A are equal. Because the proposition varies with both values, it is a dependent family. A value of the identity type is evidence of equality within the theory.

The basic constructor is reflexivity: for any x, refl(x) is evidence that x equals itself. I picture the family of equality types as a plane indexed by x and y; the reflexivity cases lie on the diagonal. The picture is an aid to intuition, not a replacement for the formal rules.

The interesting question is elimination: what can we construct from a proof p that x equals y? The dependent family now depends on x, y and the equality proof p. This is more general than the natural-number example, whose family depended on one number.

For natural numbers, the eliminator needed base and successor cases. For identity, the introduction rule has the reflexivity case. The identity eliminator, often called path induction, lets us define the dependent construction by specifying how it works for reflexivity, subject to its computation rule.

The resulting function applies when supplied with x, y and evidence p of their equality. Its computation rule says that when the evidence is refl(x), the result agrees with the case supplied for reflexivity. This is a formal rule; it should not be simplified into a claim that all equality proofs are identical.

During the talk, an audience member points out a quantifier and scope issue in a displayed formula, and I acknowledge the correction. The overall aim is to relate the identity eliminator to the induction principles already introduced.

I close with an intuition from homotopy type theory, where equality proofs can be modeled as paths. Comparing a path to a journey and reflexivity to a zero-length path evokes Zeno’s paradox; it is an illustration of the idea, not a derivation of the elimination rule.