Polymorphic lambda calculus

Read TAPL 23.

Polymorphism is not a well-defined concept; TAPL 23.2 lists several varieties of polymorphism, of which the three most commonly mentioned are:

• Subtype polymorphism is the kind seen in object-oriented programming: a reference to an object of a parent class can also refer to an object of its subclass.

• Ad hoc polymorphism is also known as function overloading: a single name refers to two different functions with different argument types.

• Parametric polymorphism, also known as genericity, is when a single function can be applied to values of many types. For example, the identity function λx.x ought to be applicable to values of any type.

Our focus here is on parametric polymorphism. As a running example, consider

let id = λx. x in {id 0, id true}

This term would evaluate to {0, true} in the untyped lambda calculus, but in the simply-typed lambda calculus, it will not type-check.

A more practical example (polymorphic lists) is given on pages 345-6. This is exactly analogous to the need for types like list<T> in C++ or LinkedList<T> in Java.

System F

System F enables polymorphism by allowing you to write terms that take types as arguments. For example:

let id = λX. λx:X. x in {id [Nat] 0, id [Bool] true}

The λX introduces a type abstraction, a term that takes a type as an argument. (Some authors use a capital Λ instead of a lowercase λ.) The [Nat] and [Bool] are type applications. (Some authors don’t use the square brackets.) They cause id to “morph” into a function on natural numbers and booleans, respectively.

Syntax and evaluation rules

t ::= ...
      λX. t   (type abstraction)
      t [X]   (type application)

T ::= ...
      X       (type variable)
      ∀X. T   (universal type)

v ::= ...
      λX. t

E ::= ...
      E [T]

(λX. t12) T2 ⟶ [X↦T2]t12   (T-TAppTAbs)

Typing rules

The typing rules for System F now include type variables in contexts (Γ). In rule T-TAbs,

  Γ, X ⊢ t2 : T2
———————————————————   (T-TAbs)
Γ ⊢ λX. t2 : ∀X. T2

the type variable X is added to the context when typing t2, just as the term variable x is added to the context when typing an abstraction. The book uses a convention (p. 342) whereby the same (type or term) variable can’t be added to the context twice; if this does happen, one of them should be renamed. Another way to get the same effect (p. 342 again) would be to add a side condition that X is not a free type variable in Γ.

The other new typing rule is

    Γ ⊢ t1 : ∀X. T12
――――――――――――――――――――――――   (T-TApp)
Γ ⊢ t1 [T2] : [X↦T2]T12

Programming in System F

System F lets us do all kinds of things that we couldn’t do in the simply-typed lambda calculus, like Church encodings of numbers, booleans, or lists (pages 347-353). In fact, we can encode product types, sum types, and even recursive types so long as the recursion is in positive position [1].

Booleans:

CBool ≡ ∀X. X → X → X
  tru ≡ λX. λt:X. λf:X. t
  fls ≡ λX. λt:X. λf:X. f

Exercise [23.4.5]: Define and. It may be helpful (and often is helpful in general) to write down the type of and first.

Numbers:

CNat ≡ ∀X. (X→X) → X → X
  c0 ≡ λX. λs:X→X. λz:X. z
  c1 ≡ λX. λs:X→X. λz:X. s z
  c2 ≡ λX. λs:X→X. λz:X. s (s z)
     ⋮

Exercise [23.4.6]: Define iszero.

Type inference?

We could also imagine an implicitly-typed System F, where the terms look just like the untyped lambda calculus, that is, no type annotations on abstractions, no type abstractions, and no type applications. This would look like the simply-typed lambda calculus with the addition of two typing rules:

 x:T ∈ Γ
—————————                            (T-Var)
Γ ⊢ x : T

  Γ, x:T1 ⊢ t2 : T2
—————————————————————                (T-Abs)
Γ ⊢ λx. t2 : T1 → T2

Γ ⊢ t1 : T11→T12    Γ ⊢ t2 : T11
—————————————————————————————————    (T-App)
        Γ ⊢ t1 t2 : T12

Γ, X ⊢ t : T
—————————————                        (T-Gen)
Γ ⊢ t : ∀X. T

 Γ ⊢ t1 : ∀X. T12
———————————————————                  (T-Inst)
Γ ⊢ t1 : [X↦T2]T12

The new rules T-Gen and T-Inst are just the rules T-TAbs and T-TApp, respectively, with type annotations, abstractions, and applications erased.

The intuition behind T-Gen is: before typing a term t, we can create a new type variable X, which may end up appearing in the type of t. (This is because T-Abs can guess a type for a term variable that uses X.) After typing t, T-Gen wraps a ∀X around its type.

The intuition behind T-Inst is: after typing t, if its type has a ∀X, we can strip it off and replace (free occurrences of) X with another type (which could be polymorphic and which could involve other type variables).

The bad news is that type reconstruction in this system is undecidable [2]. So we need to restrict the type system to make it practical for type reconstruction.