Chapter 2
Lambda calculus
The lambda calculus serves as the basis of most functional programming lan-
guages. More accurately, we might say that functional programming languages
are based on the lambda calculi (plural), since there are many variants of lambda
calculus. In this chapter we’ll introduce three of these variants, starting with
the simply typed lambda calculus (Section 2.2), moving on to System F, the
polymorphic lambda calculus (Section 2.3), and concluding with System F𝜔, a
variant of System F with type operators (Section 2.4).
𝜆→
(Section 2.2)
adding
polymorphism
��
System F
(Section 2.3)
adding
type operators
��
System F𝜔
(Section 2.4)
Figure 2.1: Chapter plan
None of the calculi in this chapter are particu-
larly suitable for programming. The simpler sys-
tems are insufficiently expressive — for example,
they have no facilities for defining data types. In
contrast, System F𝜔, the last system that we’ll
look at, has excellent abstraction facilities but
is rather too verbose for writing programs. In
OCaml, the language we’ll use for the rest of the
course, we might define the function that com-
poses two functions as follows:
fun f g x -> f (g x)
We can define the same function in System F𝜔,
but the simple logic is rather lost in a mass of
annotations:
Λ𝛼 : : ∗ .
Λ𝛽 : : ∗ .
Λ𝛾 : : ∗ .
𝜆 f :𝛼 → 𝛽 .
𝜆g :𝛾 → 𝛼 .
𝜆x :𝛾 . f (g x)
If these systems are unsuitable for program-
ming, why should we study them at all? One
reason is that many — perhaps most — of the
7
8 CHAPTER 2. LAMBDA CALCULUS
features available in modern functional program-
ming languages have straightforward translations
into System F𝜔 or other powerful variants of the
lambda calculus1. The calculi in this chapter will give us a simple and uni-
form framework for understanding many language features and programming
patterns in the rest of the course that might otherwise seem complex and arbi-
trary.
The foundational nature of System F and System F𝜔 means that we’ll see
them in a variety of roles during the course, including:
• the elaboration language for type inference in Chapter 3.
• the proof system for reasoning with propositional logic in Chapter 4.
• the setting for dualities in Chapter 5
• the background for parametricity properties in Chapter 6
• the language underlying and motivating higher-order polymorphism in
languages such as OCaml in Chapter 6
• the elaboration language for modules in Chapter 6
• the core calculus for GADTs in Chapter 8
2.1 Typing rules
We’ll present the various languages in this chapter using inference rules, which
take the following form:
premise 1 premise 2 … premise N
rule nameconclusion
This is read as follows: from proofs of premise 1, premise 2, …premise n we
may obtain a proof of conclusion using the rule rule name. Here is an example
rule, representing one of the twenty-four Aristotelian syllogisms:
all 𝑀 are 𝑃 all 𝑆 are 𝑀 modus barbaraall 𝑆 are 𝑃
The upper-case letters 𝑀 , 𝑃 , and 𝑆 in this rule are meta-variables: we may
replace them with valid terms to obtain an instance of the rule. For example,
we might instantiate the rule to
1 Some implementations of functional languages, such as the Glasgow Haskell Compiler, use
a variant of System F𝜔 as an internal language into which source programs are translated as
an intermediate step during compilation to machine code. OCaml doesn’t use this strategy,
but understanding how we might translate OCaml programs to System F𝜔 still gives us a
useful conceptual model.
2.2. SIMPLY TYPED LAMBDA CALCULUS 9
all programs are buggy all functional programs are programs
modus barbaraall functional programs are buggy
The rules that we will see in this chapter have some additional structure:
each statement, whether a premise or a conclusion, typically involves a context,
a term and a classification. For example, here is the rule →-elim2:
Γ ⊢ 𝑀 ∶ 𝐴 → 𝐵
Γ ⊢ 𝑁 ∶ 𝐴 →-elimΓ ⊢ 𝑀 𝑁 ∶ 𝐵
Both the premises and the conclusion take the form Γ ⊢ 𝑀 ∶ 𝐴, which we
can read “In the context Γ, 𝑀 has type 𝐴.” It is important to note that each
occurrence of Γ refers to the same context (and similarly for 𝑀 , 𝑁 , 𝐴, and 𝐵):
the →-elim rule says that if the term 𝑀 has type 𝐴 → 𝐵 in a context Γ, and
the term 𝑁 has type 𝐴 in the same context Γ, then the term 𝑀 𝑁 has type 𝐵
in the same context Γ. As before, Γ, 𝑀 , etc. are metavariables which we can
instantiate with particular contexts and terms to obtain facts about particular
programs.
2.2 Simply typed lambda calculus
We’ll start by looking at a minimal language. The simply typed lambda calculus
lies at the core of typed functional languages such as OCaml. Every typed
lambda calculus program is (after a few straightforward syntactic changes) a
valid program in OCaml, and every non-trivial OCaml program is built from
the constructs of the typed lambda calculus along with some “extra stuff” —
polymorphism, data types, modules, and so on — which we will cover in later
chapters.
The name “simply typed lambda calculus” is rather unwieldy, so we’ll use
the traditional and shorter name 𝜆→. The arrow → indicates the centrality of
function types 𝐴 → 𝐵.
Let’s start by looking at some simple 𝜆→ programs.
• The simplest complete program is the identity function, which simply
returns its argument. Since 𝜆→ is not polymorphic we need a separate
identity function for each type. At a given type 𝐴 the identity function is
written as follows:
𝜆x :A. x
In OCaml we write
fun x -> x
2We will often arrange premises vertically rather than horizontally.
10 CHAPTER 2. LAMBDA CALCULUS
or, if we’d like to be explicit about the type of the argument,
fun (x : a) -> x
• The compose function corresponding to the mathematical composition
of two functions is written
𝜆 f :𝐵 → 𝐶 .𝜆g :𝐴 → 𝐵 .𝜆x :𝐴 . f (g x)
for types 𝐴, 𝐵 and 𝐶. In OCaml we write
fun f g x -> f (g x)
Although simple, these examples illustrate all the elements of 𝜆→: types,
variables, abstractions, applications and parenthesization. We now turn to a
more formal definition of the calculus. For uniformity we will present both the
grammar of the language and the type rules3 as inference rules.
The elements of the lambda calculi described here are divided into three
“sorts”:
• terms, such as the function application f p. We use the letters 𝐿, 𝑀 and
𝑁 (sometimes subscripted: 𝐿1, 𝐿2, etc.) as metavariables that range over
terms, so that we can write statements about arbitrary terms: “For any
terms 𝑀 and 𝑁 …”.
• types, such as the function type ℬ → ℬ. The metavariables 𝐴 and 𝐵
range over expressions that form types. We write 𝑀 ∶ 𝐴 to say that the
term 𝑀 has the type 𝐴.
• kinds, which you can think of as the types of type expressions. The
metavariable 𝐾 ranges over kinds. We write 𝑇 ∶∶ 𝐾 to say that the type
expression 𝑇 has the kind 𝐾.
Kinds in 𝜆→ Rules that introduce kinds take the following form:
𝐾 is a kind
Kinds play little part in 𝜆→, so their structure is trivial. The later calculi
will enrich the kind structure. For now there is a single kind, called ∗.
∗-kind∗ is a kind
3Here and throughout this chapter we will focus almost exclusively on the grammar and
typing rules of the language — the so-called static semantics — and treat the dynamic seman-
tics (evaluation rules) as “obvious”. There are lots of texts that cover the details of evaluation,
if you’re interested; Pierce’s book is a good place to start.
2.2. SIMPLY TYPED LAMBDA CALCULUS 11
Kinding rules in 𝜆→ The set of types is defined inductively using rules of
the form
Γ ⊢ 𝐴 ∶∶ 𝐾
which you can read as “type 𝐴 has kind 𝐾 in environment Γ. We will have more
to say about environments shortly. In 𝜆→ there are two kinding rules, which
describe how to form types:
kind-ℬΓ ⊢ ℬ ∶∶ ∗ Γ ⊢ 𝐴 ∶∶ ∗ Γ ⊢ 𝐵 ∶∶ ∗ kind-→Γ ⊢ 𝐴 → 𝐵 ∶∶ ∗
The kind-ℬ rule introduces a base type ℬ of kind ∗. Base types correspond
to primitive types available in most programming languages, such as the types
int, float, etc. in OCaml. They will not play a very significant part in the
development, but without them we would have no way of constructing types in
𝜆→.
The kind-→ rule gives us a way of forming function types 𝐴 → 𝐵 from
types 𝐴 and 𝐵. The arrow → associates rightwards: 𝐴 → 𝐵 → 𝐶 means
𝐴 → (𝐵 → 𝐶), not (𝐴 → 𝐵) → 𝐶. We’ll use parentheses in the obvious
way when we need something other than the default associativity, but we won’t
bother to include the (entirely straightforward) rules showing where parentheses
can occur.
Using the rules kind-ℬ and kind-→ we can form a variety of function types.
For example,
• ℬ, the base type.
• ℬ → ℬ, the type of functions from ℬ to ℬ.
• ℬ → (ℬ → ℬ), the type of functions from ℬ to functions-from-ℬ-to-ℬ.
The expression ℬ → ℬ → ℬ has the same meaning.
• (ℬ → ℬ) → ℬ, the type of functions from functions-from-ℬ-to-ℬ to ℬ.
Since the syntax of types is described using logical rules we can give formal
derivations for particular types. For example, the type (ℬ → ℬ) → ℬ can be
derived as follows:
kind-ℬΓ ⊢ ℬ ∶∶ ∗ kind-ℬΓ ⊢ ℬ ∶∶ ∗ kind-→Γ ⊢ ℬ → ℬ ∶∶ ∗ kind-ℬΓ ⊢ ℬ ∶∶ ∗ kind-→Γ ⊢ (ℬ → ℬ) → ℬ ∶∶ ∗
Environment rules in 𝜆→ Environments associate variables with their clas-
sifiers. In 𝜆→ there is only one sort of variables, for terms, and so environments
associate term variables with types. Later sections extend the type language
with variables, too; environments then additionally map type variables to kinds.
Rules for forming environments have the form
Γ is an environment
In 𝜆→ there are two rules for forming environments:
12 CHAPTER 2. LAMBDA CALCULUS
Γ-·· is an environment Γ is an environment Γ ⊢ 𝐴 ∶∶ ∗ Γ-∶Γ, 𝑥∶𝐴 is an environment
The rule Γ-· introduces an empty environment. The rule Γ-∶ extends an
existing environment Γ with a binding 𝑥∶𝐴 – that is, it associates the variable
𝑥 with the type 𝐴. (We use the letters 𝑥, 𝑦, 𝑧 for variables.) We will be
a little informal in our treatment of environments, sometimes viewing them as
sequences of bindings and sometimes as sets of bindings. We’ll also make various
simplifying assumptions; for example, we’ll assume that each variable can only
occur once in a given environment. With more care it’s possible to formalise
these assumptions, but the details are unnecessary for our purposes here.
As with types, we can use Γ-· and Γ-∶ to form a variety of environments. For
example,
• The empty environment ·
• An environment with two variable bindings ·, 𝑥∶ℬ, 𝑓∶(ℬ → ℬ)
Typing rules in 𝜆→ The rule Γ-∶ shows how to add variables to an envi-
ronment. We’ll also need a way to look up variables in an environment. The
following rule is the first of the three 𝜆→ typing rules, which have the form
Γ ⊢ 𝑀 ∶ 𝐴 (read “the term 𝑀 has the type 𝐴 in environment Γ”) and describes
how to form terms:
𝑥∶𝐴 ∈ Γ tvarΓ ⊢ 𝑥 ∶ 𝐴
The tvar rule makes it possible to type open terms (i.e. terms with free
variables). If the environment Γ contains the binding 𝑥∶𝐴 then the term 𝑥 has
the type 𝐴 in Γ.
The remaining two typing rules for 𝜆→ show how to introduce and eliminate
terms of function type — that is, how to define and apply functions.
Γ, 𝑥∶𝐴 ⊢ 𝑀 ∶ 𝐵
→-introΓ ⊢ 𝜆𝑥∶𝐴.𝑀 ∶ 𝐴 → 𝐵
Γ ⊢ 𝑀 ∶ 𝐴 → 𝐵
Γ ⊢ 𝑁 ∶ 𝐴 →-elimΓ ⊢ 𝑀 𝑁 ∶ 𝐵
The introduction rule →-intro shows how to form a term 𝜆𝑥∶𝐴.𝑀 of type
𝐴 → 𝐵. You can read the rule as follows: “the term 𝜆𝑥∶𝐴.𝑀 has type 𝐴 → 𝐵
in Γ if its body 𝑀 has type 𝐵 in Γ extended with 𝑥∶𝐴”. Since we are introducing
the → operator, the rule has the function arrow → below the line but not above
it.
The elimination rule →-elim shows how to apply terms of function type.
The environment Γ is the same throughout the rule, reflecting the fact that
no variables are bound by the terms involved. Since we are eliminating the →
operator, the rule has the function arrow → above the line but not below it.
2.2. SIMPLY TYPED LAMBDA CALCULUS 13
The →-intro and →-elim form the first introduction-elimination pair4. We’ll
see many more such pairs as we introduce further type and kind constructors.
We illustrate the typing rules by giving derivations for the identity and
compose functions (Figures 2.2 and 2.3)5
2.2.1 Adding products
Interesting programs typically involve more than functions. Useful program-
ming languages typically provide ways of aggregating data together into larger
structures. For example, OCaml offers various forms of variants, tuples and
records, besides more elaborate constructs such as modules and objects. The
𝜆→ calculus doesn’t support any of these: there are no built-in types beyond
functions, and its abstraction facilities are too weak to define interesting new
constructs. In order to make the language a little more realistic we therefore
introduce a built-in type of binary pairs (also called “products”).
As before, we’ll start by giving some programs that we can write using
products:
• An apply function, that applies the first component of a pair to the second:
𝜆p : (A→B)×A. fst p (snd p)
In OCaml we write
fun ( f , p) -> f p
• A dup function that builds a pair with equal components:
𝜆x :A. ⟨x , x⟩
In OCaml we write
fun x -> (x , x)
• The (bi)map function for pairs:
𝜆 f :A→C.𝜆g .B→C.𝜆p .A×B. ⟨ f fst p , g snd p⟩
In OCaml we write
fun f g (x , y) -> ( f x , g y)
• The function which swaps the elements of a pair:
4It is possible to consider the environment and variable-lookup rules as an introduction
and elimination pair for environments, but we won’t take this point any further here.
5While the derivations may appear complex at first glance, they are constructed mechani-
cally from straightforward applications of the three typing rules for 𝜆→. If typing derivations
featured extensively in the course we might adopt various conventions to make them simpler
to write down, since much of the apparent complexity is just notational overhead.
14 CHAPTER 2. LAMBDA CALCULUS
·,𝑥∶𝐴
⊢
𝑥
∶𝐴
→
-intro
·⊢
𝜆𝑥∶𝐴
.𝑥
∶𝐴
→
𝐴
F
igure
2.2:
T
he
derivation
for
the
identity
function.
·,𝑓∶𝐵
→
𝐶
,𝑔∶𝐴
→
𝐵
,𝑥∶𝐴
⊢
𝑓
∶𝐵
→
𝐶
·,𝑓∶𝐵
→
𝐶
,𝑔∶𝐴
→
𝐵
,𝑥∶𝐴
⊢
𝑔
∶𝐴
→
𝐵
·,𝑓∶𝐵
→
𝐶
,𝑔∶𝐴
→
𝐵
,𝑥∶𝐴
⊢
𝑥
∶𝐴
→
-elim
·,𝑓∶𝐵
→
𝐶
,𝑔∶𝐴
→
𝐵
,𝑥∶𝐴
⊢
𝑔
𝑥
∶𝐵
→
-elim
·,𝑓∶𝐵
→
𝐶
,𝑔∶𝐴
→
𝐵
,𝑥∶𝐴
⊢
𝑓
(𝑔
𝑥)∶𝐶
→
-intro
·,𝑓∶𝐵
→
𝐶
,𝑔∶𝐴
→
𝐵
⊢
𝜆𝑥∶𝐴
.𝑓
(𝑔
𝑥)∶𝐴
→
𝐶
→
-intro
·,𝑓∶𝐵
→
𝐶
⊢
𝜆𝑔∶𝐴
→
𝐵
.𝜆𝑥∶𝐴
.𝑓
(𝑔
𝑥)∶(𝐴
→
𝐵
)→
𝐴
→
𝐶
→
-intro
·⊢
𝜆𝑓∶𝐵
→
𝐶
.𝜆𝑔∶𝐴
→
𝐵
.𝜆𝑥∶𝐴
.𝑓
(𝑔
𝑥)∶(𝐵
→
𝐶
)→
(𝐴
→
𝐵
)→
𝐴
→
𝐶
F
igure
2.3:
T
he
derivation
for
com
pose
2.2. SIMPLY TYPED LAMBDA CALCULUS 15
𝜆p :A×B. ⟨snd p , fst p⟩
In OCaml we write
fun (x , y) -> (y , x)
Kinding rules for × There is a new way of forming types 𝐴 × 𝐵, and so we
need a new kinding rule.
Γ ⊢ 𝐴 ∶∶ ∗ Γ ⊢ 𝐵 ∶∶ ∗ kind-×Γ ⊢ 𝐴 × 𝐵 ∶∶ ∗
The kind-× rule is entirely straightforward: if 𝐴 and 𝐵 have kind ∗, then so
does 𝐴 × 𝐵.
Typing rules for × There are three new typing rules:
Γ ⊢ 𝑀 ∶ 𝐴
Γ ⊢ 𝑁 ∶ 𝐵 ×-introΓ ⊢ ⟨𝑀, 𝑁⟩ ∶ 𝐴 × 𝐵
Γ ⊢ 𝑀 ∶ 𝐴 × 𝐵 ×-elim-1Γ ⊢ fst 𝑀 ∶ 𝐴
Γ ⊢ 𝑀 ∶ 𝐴 × 𝐵 ×-elim-2Γ ⊢ snd 𝑀 ∶ 𝐵
The ×-intro rule shows how to build pairs: a pair ⟨𝑀, 𝑁⟩ of type 𝐴 × 𝐵 is
built from terms 𝑀 and 𝑁 of types 𝐴 and 𝐵.
The ×-elim-1 and ×-elim-2 rules show how to deconstruct pairs. Given a
pair 𝑀 of type 𝐴 × 𝐵, fst M and snd M are respectively the first and second
elements of the pair. Unlike in OCaml, fst and snd are “keywords” rather than
first-class functions. For particular types 𝐴 and 𝐵 we can define abstractions
𝜆p∶𝐴 × 𝐵.fst p and 𝜆p∶𝐴 × 𝐵.snd p, but we do not yet have the polymorphism
required to give definitions corresponding to the polymorphic OCaml functions:
val f s t : ’ a * ’b -> ’a
let f s t (a , _) = a
val snd : ’ a * ’b -> ’b
let snd (_, b) = b
2.2.2 Adding sums
Product types correspond to a simple version of OCaml’s records and tuples.
We next extend 𝜆→ with sum types, which correspond to a simple version of
variants.
Here are some programs that we can write with 𝜆→ extended with sums:
• The (bi-)map function over sums:
𝜆 f :A→C.𝜆g :B→C.𝜆s :A+B. case s of x . f x | y . g y
In OCaml we write
16 CHAPTER 2. LAMBDA CALCULUS
fun f g s -> match s with In l x -> f x | Inr y -> g y
• The function of type A+B→B+A which swaps the inl and inr constructors:
𝜆s :A+B. case s of x . inr [B] x | y . inl [A] y
In OCaml we write
function In l x -> Inr x | Inr y -> In l y
• The function of type A+A→A that projects from either side of a sum:
𝜆s :A+A. case s of x . x | y . y
In OCaml we write
function In l x -> x | Inr y -> y
Kinding rules for + The kinding rule for sum types follows the familiar
pattern:
Γ ⊢ 𝐴 ∶∶ ∗ Γ ⊢ 𝐵 ∶∶ ∗ kind-+Γ ⊢ 𝐴 + 𝐵 ∶∶ ∗
Typing rules for + There are three new typing rules:
Γ ⊢ 𝑀 ∶ 𝐴 +-intro-1Γ ⊢ inl [𝐵] 𝑀 ∶ 𝐴 + 𝐵
Γ ⊢ 𝑁 ∶ 𝐵 +-intro-2Γ ⊢ inr [𝐴] 𝑁 ∶ 𝐴 + 𝐵
Γ ⊢ 𝐿 ∶ 𝐴 + 𝐵
Γ, 𝑥∶𝐴 ⊢ 𝑀 ∶ 𝐶
Γ, 𝑦∶𝐵 ⊢ 𝑁 ∶ 𝐶
+-elimΓ ⊢ case 𝐿 of 𝑥.𝑀 | 𝑦.𝑁 ∶ C
The +-intro-1 and +-intro-2 rules show how to build values of sum type by
injecting with inl or inr. In order to maintain the property that each term has
a unique type we also require a type argument to inl and inr6
The +-elim rule shows how to deconstruct sums. We can deconstruct sum
values 𝐿 of type 𝐴+𝐵 if we can deconstruct both the left and the right summand.
Given an OCaml variant definition
type plus = In l of a | Inr of b
the case expression
case 𝐿 of x .𝑀 | y .𝑁
corresponds to the OCaml match statement
match l with In l x → m | Inr y → n
There is an appealing symmetry between the definitions of products and
sums. Products have one introduction rule and two elimination rules; sums
have two introduction rules and one elimination rule. We shall consider this
point in more detail in chapters 4 and 5.
6These kinds of annotations are not needed in OCaml; can you see why?
2.3. SYSTEM F 17
2.3 System F
The simply typed lambda calculus 𝜆→ captures the essence of programming
with functions as first-class values, an essential feature of functional program-
ming languages. Our next calculus, System F (also known as the polymorphic
lambda calculus) captures another fundamental feature of typed functional pro-
gramming languages like OCaml and Haskell: parametric polymorphism.
We have already seen an example of the problems that arise in languages
that lack support for parametric polymorphism. In Section 2.2.1 the fst and
snd operations which project the elements of a pair were introduced as built-in
operators with special typing rules. It would be preferable to be able to define
fst and snd using the other features of the language, but it is clear that they
cannot be so defined, since 𝜆→ lacks even the facilities necessary to express their
types. A similar situation often arises during the development of a programming
language: the language is insufficiently expressive to support a feature that is
useful or even essential for writing programs. The most pragmatic solution is
often to add new built-in operations for common cases, as we have done with
products7. In this chapter we take the alternative approach of systematically
enriching the core language until it is sufficiently powerful to define new data
types directly.
The difficulties caused by the lack of polymorphism go beyond pairs. We
introduced 𝜆→ by showing how to write the identity and compose functions and
comparing the implementations with the corresponding OCaml code. In fact,
the comparison is a little misleading: in OCaml it is possible to define a single
identity function and a single compose function that work at all types, whereas
in 𝜆→ we must introduce a separate definition for each type. As the following
examples show, System F allows us to define the functions in a way that works
for all types.
• The polymorphic identity function of type ∀𝛼∶∶ ∗ .𝛼 → 𝛼:
Λ𝛼 : : ∗ .𝜆x :𝛼 . x
• The polymorphic compose function of type ∀𝛼∶∶∗.∀𝛽∶∶∗.∀𝛾∶∶∗.(𝛽 → 𝛾) →
(𝛼 → 𝛽) → 𝛼 → 𝛾:
Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .Λ𝛾 : : ∗ .𝜆 f :𝛽 → 𝛾 .𝜆g :𝛼 → 𝛽 .𝜆x :𝛼 . f (g x)
• The polymorphic apply function of type ∀𝛼∶∶ ∗ .∀𝛽∶∶ ∗ .(𝛼 → 𝛽) × 𝛼 → 𝛽:
Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆p : ( 𝛼 → 𝛽)×𝛼 . fst p (snd p)
To put it another way, we can now use abstraction within the calculus (∀𝛼 ∶∶
∗.𝐴) where we previously had to use abstraction about the calculus (For all types
𝐴 …).
7 Some examples from real languages: OCaml has a polymorphic equality operation that
works for all first-order types, but that cannot be defined within the language; Haskell’s
deriving keyword supports automatically creating instances of a fixed number of built-in type
classes; C99 provides a number of type-generic macros which work across numeric types, but
does not offer facilities that allow the user to define such macros.
18 CHAPTER 2. LAMBDA CALCULUS
Kinding rules for ∀ As the examples show, System F extends 𝜆→ with a
type-level operator ∀𝛼∶∶ ∗ .− that binds a variable 𝛼 within a particular scope.
There are two new kinding rules:
Γ, 𝛼∶∶𝐾 ⊢ 𝐴 ∶∶ ∗
kind-∀Γ ⊢ ∀𝛼∶∶𝐾.𝐴 ∶∶ ∗
𝛼∶∶𝐾 ∈ Γ tyvarΓ ⊢ 𝛼 ∶∶ 𝐾
The kind-∀ rule builds universal types ∀𝛼∶∶𝐾.𝐴. The type ∀𝛼∶∶𝐾.𝐴 has kind
∗ under an environment Γ if the type 𝐴 has kind ∗ under Γ extended with an
entry for 𝛼.
The tyvar rule is a type-level analogue of the tvar rule: it allows type vari-
ables to appear within type expressions, making it possible to build open types
(i.e. types with free variables). If the environment Γ contains the binding 𝛼∶∶𝐾
then the type 𝛼 has the kind 𝐾 in Γ
These rules involve a new kind of variable into the language. Type vari-
ables are bound by ∀ and (as we shall see) by Λ, and can be used in place
of concrete types in expressions. It is important to distinguish between type
variables (for which we write 𝛼, 𝛽, 𝛾) and metavariables (written 𝐴, 𝐵, 𝐶).
We use metavariables when we wish to talk about types without specifying any
particular type, but type variables are part of System F itself, and can appear
in concrete programs.
Environment rules for ∀ The tyvar rule requires that we extend the defi-
nition of environments to support type variable bindings (associations of type
variables with their kinds):
Γ is an environment 𝐾 is a kind Γ-∶∶Γ, 𝛼∶∶𝐾 is an environment
Typing rules for ∀ Since we have a new type constructor ∀, we need a new
pair of introduction and elimination rules:
Γ, 𝛼∶∶𝐾 ⊢ 𝑀 ∶ 𝐴
∀-introΓ ⊢ Λ𝛼∶∶𝐾.𝑀 ∶ ∀𝛼∶∶𝐾.𝐴 Γ ⊢ 𝑀 ∶ ∀𝛼∶∶𝐾.𝐴 Γ ⊢ 𝐵 ∶∶ 𝐾 ∀-elimΓ ⊢ 𝑀 [𝐵] ∶ 𝐴[𝛼 ∶= 𝐵]
The ∀-intro rule shows how to build values of type ∀𝛼∶∶𝐾.𝐴 — that is,
polymorphic values. The term Λ𝛼∶∶𝐾.𝑀 has type ∀𝛼∶∶𝐾.𝐴 in Γ if the body 𝑀
has the type 𝐴 in Γ extended with a binding for 𝛼.
The ∀-elim rule shows how to use values of polymorphic type via a second
form of application: applying a (suitably-typed) term to a type. If 𝑀 has a
polymorphic type ∀𝛼∶∶∗ .𝐴 then we can apply it to the type 𝐵 (also written “in-
stantiate it at type B”) to obtain a term of type 𝐴[𝛼 ∶= 𝐵] — that is, the type
𝐴 with all free occurrences of 𝛼 replaced by the type 𝐵. (Once again, substi-
tution needs to be carefully defined to avoid inadvertently capturing variables,
and once again we omit the details.)
2.3. SYSTEM F 19
There is nothing in the OCaml language that quite corresponds to the ex-
plicit introduction and elimination of polymorphic terms. However, one way
to view OCaml’s implicit polymorphism is as a syntactic shorthand for (some)
System F programs, where constructs corresponding to ∀-intro and ∀-elim are
automatically inserted by the type inference algorithm. We will consider this
view in more detail in Chapter 3 and describe OCaml’s alternatives to Sys-
tem F-style polymorphism in Chapter 6.
2.3.1 Adding existentials
For readers of a logical bent the name of the new type operator ∀ is suggestive.
Might there be a second family of type operators ∃? It turns out that there
is indeed a useful notion of ∃ types: just as ∀ is used for terms which can be
instantiated at any type, ∃ can be used to form types for which we have some
implementation, but prefer to leave the details abstract. These existential types
play several important roles in programming, and we will return to them on
various occasions throughout the course. For example,
• There is a close connection between the ∀ and ∃ operators in logic and the
type operators that we introduce here, which we will explore in Chapter 4.
• Just as in logic, there is also a close connection between the ∀ operator
and the ∃ operator, which we will consider in more detail in Chapter 5.
• The types of modules can be viewed as a kind of existential type, as we
shall see in chapter 6.
• OCaml’s variant types support a form of existential quantification, as we
shall see in Chapter 6.
As we shall see in Chapter 5, it is possible to encode existential types using
universal types. For now we will find it more convenient to introduce them
directly as an extension to System F.
Kinding rules for ∃ Adding existentials involves one new kinding rule, which
says that ∃𝛼∶∶𝐾.𝐴 has kind ∗ if 𝐴 has kind ∗ in an extended environment:
Γ, 𝛼∶∶𝐾 ⊢ 𝐴 ∶∶ ∗
kind-∃Γ ⊢ ∃𝛼∶∶𝐾.𝐴 ∶∶ ∗
Typing rules for ∃ The typing rules for ∃ follow the familiar introduction-
elimination pattern:
Γ ⊢ 𝑀 ∶ 𝐴[𝛼 ∶= 𝐵] Γ ⊢ ∃𝛼∶∶𝐾.𝐴 ∶∶ ∗
∃-introΓ ⊢ pack 𝐵, 𝑀 as ∃𝛼∶∶𝐾.𝐴 ∶ ∃𝛼∶∶𝐾.𝐴
Γ ⊢ 𝑀 ∶ ∃𝛼∶∶𝐾.𝐴
Γ, 𝛼∶∶𝐾, 𝑥∶𝐴 ⊢ 𝑀 ′ ∶ 𝐵
∃-elimΓ ⊢ open 𝑀 as 𝛼, 𝑥 in 𝑀 ′ ∶ 𝐵
20 CHAPTER 2. LAMBDA CALCULUS
The ∃-intro rule shows how to build values of existential type using a new
construct, pack. A pack expression associates two types with a particular term
𝑀 : if 𝑀 may be given the type 𝐴[𝛼 ∶= 𝐵] in the environment Γ for suitable
𝐴, 𝛼 and 𝐵 then we may pack 𝑀 together with 𝐵 under the type ∃𝛼∶∶𝐾.𝐴. It
is perhaps easiest to consider the conclusion first: the expression pack B,M as
∃𝛼∶∶𝐾.𝐴 has the existential type ∃𝛼∶∶𝐾.𝐴 if replacing every occurrence of 𝛼 in
𝐴 with 𝐵 produces the type of 𝑀 .
The ∃-elim rule shows how to use values of existential type using a new
construct open. “Opening” a term 𝑀 with the existential type ∃𝛼∶∶𝐾.𝐴 involves
binding the existential variable 𝛼 to the type 𝐴 and a term variable 𝑥 to the
term 𝑀 within some other expression 𝑀 ′. It is worth paying careful attention
to the contexts of the premises and the conclusion. Since 𝛼 is only in scope for
the typing of 𝑀 ′ it cannot occur free in the result type of the conclusion 𝐵.
That is, the existential type is not allowed to “escape” from the body of the
open.
∃ examples Existential types are more complex than the other constructs
we have introduced so far, so we will consider several examples. Each of our
examples encodes a data type using the constructs available in System F.
2.3.2 Encoding data types in System F
Our first example is a definition of the simplest datatype — that is, the “unit”
type with a single constructor and no destructor. OCaml has a built-in unit
type, but if it did not we might define its signature as follows:
type t
val u : t
The following System F expression builds a representation of the unit type
using the type of the polymorphic identity function, which also has a single
inhabitant:
pack (∀𝛼 : : ∗ .𝛼 → 𝛼 ,
Λ𝛼 .𝜆a :𝛼 . a )
as ∃𝜐 : : ∗ .𝜐
In the examples that follow we will write 1 to denote the unit type and ⟨⟩ to
denote its sole inhabitant.
Our next example defines a simple abstract type of booleans. OCaml has a
built-in boolean type, but if it did not we might define a signature for bools as
follows:
type t
val f f : t
val t t : t
val _if_ : t → ’ a → ’ a → ’ a
That is: there are two ways of constructing boolean values, tt and ff , and
a branching construct _if_ which takes a boolean and two alternatives, one of
which it returns. We might represent boolean values using a variant type:
2.3. SYSTEM F 21
type boolean =
False : boolean
| True : boolean
Using boolean we can give an implementation of the signature:
module Bool :
sig
type t
val f f : t
val t t : t
val _if_ : t → ’ a → ’ a → ’ a
end =
struct
type t = boolean
let f f = False
let t t = True
let _if_ cond _then_ _else_ =
match cond with True → _then_ | False → _else_
end
If we ask OCaml to type-check the body of the module, omitting the signa-
ture, it produces the following output:
sig
type t = boolean
val f f : boolean
val t t : boolean
val _if_ : boolean -> ’a -> ’a -> ’a
end
The relationship between the inferred module type and the signature cor-
responds closely to the relationship between the supplied existential type and
the type of the body in the rule ∃-intro. Substituting the actual representation
type boolean for the abstract type t in the signature gives the module type of
the body. We will explore this behaviour more fully in Chapter 6.
Just as we can use variants to define booleans in OCaml, we can use sums to
define booleans in System F. Here is a definition analogous to the Bool module
above, using the left injection for false and the right injection for true:
pack (1+1,
⟨inr [ 1 ] ⟨⟩ ,
⟨ inl [ 1 ] ⟨⟩ ,
𝜆b : Bool .Λ𝛼 : : ∗ .𝜆r :𝛼 .𝜆s :𝛼 . case b of x . s | y . r⟩⟩)
as ∃𝛽 : : ∗ .
𝛽 ×
𝛽 ×
𝛽 → ∀𝛼 : : ∗ .𝛼 → 𝛼 .𝛼
The unit and boolean examples encode data types with small fixed num-
bers of inhabitants. However System F is also sufficiently powerful to encode
datatypes with infinitely many members, as we now proceed to show.
A type representing the natural numbers can be defined in OCaml as a
variant with two constructors:
type nat =
Zero : nat
22 CHAPTER 2. LAMBDA CALCULUS
| Succ : nat -> nat
Using these constructors we can represent every non-negative integer: for
example, the number three is represented as follows:
let three = Succ (Succ (Succ Zero ) )
We can encode the natural numbers in System F as follows:
pack (∀𝛼 : : ∗ .𝛼 →(𝛼 → 𝛼)→ 𝛼 ,
⟨Λ𝛼 : : ∗ .𝜆z :𝛼 .𝜆s :𝛼 → 𝛼 . z ,
⟨𝜆n :∀𝛼 : : ∗ .𝛼 →(𝛼 → 𝛼)→ 𝛼 .
Λ𝛼 : : ∗ .𝜆z :𝛼 .𝜆s :𝛼 → 𝛼 . s (n [𝛼 ] z s ) ,
⟨𝜆n :∀𝛼 : : ∗ .𝛼 →(𝛼 → 𝛼)→ 𝛼 . n⟩⟩⟩)
as ∃ℕ ∶∶ ∗.
ℕ ×
(ℕ → ℕ) ×
(ℕ → ∀𝛼 .𝛼 →(𝛼 → 𝛼)→ 𝛼)
As for booleans there are two constructors corresponding to the constructors
of the data type and a branching operation (which we will call foldℕ) which makes
it possible to define functions that discriminate between different numbers. The
branching operation accepts a natural number of type ℕ, a type argument 𝛼
specifying the type of the result, a value of type 𝛼 to return in case the input
is zero and a function of type 𝛼 → 𝛼 to use in case the input is the successor
of some other number 𝑛. Using foldℕ we might define the function which tests
whether a number is equal to zero by instantiating the result type with Bool and
passing suitable arguments for the zero and successor cases:
𝜆m:ℕ .𝜆n :ℕ . f o ldℕ m [ Bool ] true (𝜆b : Bool . f a l s e )
Similarly we might define the addition function using foldℕ by instantiating
the result type with ℕ:
𝜆m:ℕ .𝜆n :ℕ . f o ldℕ m [ℕ ] n succ
2.4 System F𝜔
We motivated the introduction of System F with the observation that adding
products to 𝜆→ involves special typing rules for fst and snd, since 𝜆→ does not
support polymorphic operations. System F addresses this deficiency: we can
express the types of fst and snd within the calculus itself, making it possible
to abstract the operations. For example, here is a polymorphic function which
behaves like fst:
Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆p :𝛼 × 𝛽 . fst p
However, System F shares with 𝜆→ the problem that it is not possible to
define a parameterised type of binary pairs within the calculus: we can build
separate, unrelated definitions for Bool×Bool, ℕ×Bool, ℕ × ℕ, and so on, but no
single definition that suffices for all these types. The difficulty lies in the kind
of the × operator. As the kind-× rule (Section 2.2.1) shows, × is applied to two
type expressions of kind ∗ to build another such type expression. System F does
2.4. SYSTEM FΩ 23
not offer a way of introducing this type of parameterised type constructor, but
the calculus that we now consider extends System F with exactly this facility.
The calculus System F𝜔 adds a third type of 𝜆-abstraction to the two forms
that are available in System F. We already have 𝜆x:A.M, which abstracts terms
to build terms, and Λ𝛼::K.M, which abstracts types to build terms. The new
abstraction form 𝜆𝛼::K.A abstracts types to build types.
Up until now the structure of kinds has been trivial, limited to a single kind
∗, to which all type expressions belonged. We now enrich the set of kinds with
a new operator ⇒, allowing us to construct kinds which contain type operators
and even higher-order type operators. The new type abstraction form 𝜆𝛼::K.A
allows us to populate these new kinds with type operators. We’ll also add a
corresponding type application form A B for applying type operators.
Let’s start by looking at some examples of type expressions that we can
build in this enriched language.
• The kind ∗⇒∗⇒∗ expresses the type of binary type operators such as × and
+. The following type expression abstracts such an operator and applies
it twice to the unit type 1:
𝜆𝜑 : : ∗⇒∗⇒∗ .𝜑 1 1
• The kind (∗⇒∗)⇒∗⇒∗ expresses the type of type operators which are pa-
rameterised by a unary type operator and by a type. The following type
expression, which applies the abstracted type operator twice to the argu-
ment, is an example:
𝜆𝜑 : : ∗⇒∗ .𝜆𝛼 : : ∗ .𝜑 (𝜑 𝛼)
It is still the case that only type expressions of kind ∗ are inhabited by terms.
We will continue to use the name “type” only for type expressions of kind ∗.
Kinds in System F𝜔 There is one new rule for introducing kinds:
𝐾1 is a kind 𝐾2 is a kind ⇒-kind𝐾1 ⇒ 𝐾2 is a kind
It is worth noting that the addition of new kinds retroactively enriches the
existing rules. For example, in the kind-∀ rule the type variable 𝛼 is no longer
restricted to the kind ∗.
Kinding rules for System F𝜔 We have two new ways of forming type ex-
pressions, so we need two new kinding rules. The new rules form an introduction-
elimination pair for the new kind constructor ⇒, the first such pair at the type
level.
24 CHAPTER 2. LAMBDA CALCULUS
Γ, 𝛼∶∶𝐾1 ⊢ 𝐴 ∶∶ 𝐾2 ⇒-introΓ ⊢ 𝜆𝛼∶∶𝐾1.𝐴 ∶∶ 𝐾1 ⇒ 𝐾2
Γ ⊢ 𝐴 ∶∶ 𝐾1 ⇒ 𝐾2
Γ ⊢ 𝐵 ∶∶ 𝐾1 ⇒-elimΓ ⊢ 𝐴 𝐵 ∶∶ 𝐾2
The introduction rule ⇒-intro shows how to form a type expression 𝜆𝛼∶∶𝐾1.𝐴
of kind 𝐾1 ⇒ 𝐾2. Comparing it with the corresponding rule for terms, →-intro,
reveals that the structure of the two rules is the same.
The elimination rule ⇒-elim shows how to apply type expressions to type
expressions, and follows the pattern of the corresponding term-level application
rule, →-elim.
Type equivalence We have passed over one important aspect of type-level
abstraction. The ⇒-elim rule specifies that the domain kind of the type operator
and the kind of the operand should be the same. But what do we mean by
“the same”? In the earlier calculi a simple syntactic equality would do the
trick: two types are the same if they are built from the same symbols in the
same order (after removing any superfluous parentheses). Now that we have
added type-level operations we need a more “semantic” notion of equality: two
type expressions should be considered the same if they are the same once fully
reduced — i.e., once all applications of 𝜆-expressions have been eliminated. For
simplicity we won’t go into any more detail about this aspect of System F𝜔, but
it is essential to a fully correct formal treatment.
2.4.1 Encoding data types in System F𝜔
The new type-level programming facilities introduced in System F𝜔 significantly
increase the expressive power of the language, as we will see in the following
examples.
Encoding sums in System F𝜔 We are finally able to encode the definitions
of the sum and product abstractions directly within the calculus itself. Here is
an encoding of sums using polymorphism. We expose a binary type operator
and functions corresponding to the two constructors inl and inl, and to case.
pack 𝜆𝛼 : : ∗ .𝜆𝛽 : : ∗ .∀𝛾 : : ∗ . ( 𝛼 → 𝛾 )→(𝛽 → 𝛾 )→ 𝛾 ,
⟨Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆v :𝛼 .Λ𝛾 : : ∗ .𝜆 l :𝛼 → 𝛾 .𝜆r :𝛽 → 𝛾 . l v
⟨Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆v :𝛽 .Λ𝛾 : : ∗ .𝜆 l :𝛼 → 𝛾 .𝜆r :𝛽 → 𝛾 . r v
Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆c :∀𝛾 : : ∗ . ( 𝛼 → 𝛾 )→(𝛽 → 𝛾 )→ 𝛾 . c⟩⟩
as ∃𝜑 : : ∗⇒∗⇒∗ .
∀𝛼 : : ∗ .∀𝛽 : : ∗ .𝛼 → 𝜑 𝛼 𝛽
× ∀𝛼 : : ∗ .∀𝛽 : : ∗ .𝛽 → 𝜑 𝛼 𝛽
× ∀𝛼 : : ∗ .∀𝛽 : : ∗ .𝜑 𝛼 𝛽 → ∀𝛾 : : ∗ . ( 𝛼 → 𝛾 )→(𝛽 → 𝛾 )→ 𝛾
The encoding follows the same pattern as ℕ: a sum value is represented as
a function with two parameters, one for each sum constructor. A left injection
inl M is represented as a function that passes 𝑀 to its first argument; a right
injection inr M as a function that passes 𝑀 to its second argument. Observe
2.4. SYSTEM FΩ 25
that the addition of higher kinds allows us to use create higher-kinded existential
variables: 𝜑 has kind ∗⇒∗⇒∗.
As we saw when we extended 𝜆→ with polymorphism, the extra abstraction
facilities enable us to express in the language what we could previously only ex-
press in statements about the language. We could previously say things like “For
all binary type operators 𝜙”; now we can abstract over binary type operators
within the calculus itself.
Encoding lists in System F𝜔 There is a simple connection between the Bool
type that we could encode in System F and the sum type that we have encoded
in System F𝜔: instantiating the arguments of the sum type with 1 gives us Bool.
Similarly, we could encode ℕ in System F, but System F𝜔 allows us to encode
a list type, which we can think of as a kind of parameterised version of ℕ.
A definition of lists in OCaml has two constructors, Nil and Cons:
type ’ a l i s t =
Nil : ’ a l i s t
| Cons : ’ a * ’a l i s t -> ’a l i s t
We therefore encode lists in System F𝜔 using a function of two arguments,
whose types reflect the types of the corresponding constructors8:
List = 𝜆𝛼 : : ∗ .∀𝜑 : : ∗⇒∗ .𝜑 𝛼 →(𝛼 → 𝜑 𝛼 → 𝜑 𝛼)→ 𝜑 𝛼
The constructor for the empty list is represented as a function which takes
two arguments and returns the first:
n i l = Λ𝛼 : : ∗ .Λ𝜑 : : ∗⇒∗ .𝜆n :𝜑 𝛼 .𝜆c :𝛼 → 𝜑 𝛼 → 𝜑 𝛼 . n ;
The function corresponding to Cons takes two additional arguments x and xs
corresponding to the arguments of the Cons constructor:
cons = Λ𝛼 : : ∗ .𝜆x :𝛼 .𝜆xs : List � .
Λ𝜑 : : ∗⇒∗ .𝜆n :𝜑 𝛼 .𝜆c :𝛼 → 𝜑 𝛼 → 𝜑 𝛼 .
c x ( xs [𝜑 ] n c ) ;
Finally, the destructor for lists corresponds to OCaml’s List.fold_right func-
tion:
f o ldL i s t = Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆c :𝛼 → 𝛽 → 𝛽 .𝜆n :𝛽 .𝜆 l : L i st 𝛼 . l [𝜆𝛾 : : ∗ .𝛽 ] n c
The analogue of the addition function that we defined using the encoding of
ℕ is the binary append function for lists, which may be defined as follows:
append = Λ𝛼 : : ∗ .
𝜆 l : L i st 𝛼 .𝜆r : L ist 𝛼 .
f o ldL i s t [𝛼 ] [ L i st 𝛼 ] ( cons [𝛼 ] ) l r
We have seen how System F𝜔 makes it possible to encode a number of
common data types: unit, booleans, numbers, sums and lists. However, these
encodings use relatively little of the expressive power of the calculus. We will
finish with two slightly more exotic examples which illustrate some of the things
that become possible with first class polymorphism and type-level abstraction.
8We could easily define lists using an existential type as we have done for the other encod-
ings, but as the types grow larger the monolithic pack expressions become less readable, so
we will switch at this point to presenting the components of the encoding individually
26 CHAPTER 2. LAMBDA CALCULUS
Encoding non-regular data types in System F𝜔 Most data types used
in OCaml are “regular”: when defining of a type t, all occurrences of t within
the definition are instantiated with the same parameters. For example, the tree
constructor occurs four times on the right hand side of the following definition
of a tree type, and at each occurrence it is applied to the parameter ’a:
type ’ a t ree =
Empty : ’ a tree
| Tree : ’ a t ree * ’a * ’a tree -> ’a tree
In contrast, in the following definition the argument of SuccP has the type
(’a * ’a) perfect: the type constructor perfect is applied to the pair type ’a * ’a
rather than to the parameter ’a:
type ’ a per f ec t =
ZeroP : ’ a -> ’a per f ec t
| SuccP : ( ’ a * ’a) per f ec t -> ’a per f ec t
This kind of non-regular or “nested” type definition makes it possible to
represent constraints on data that are difficult or impossible to capture using
regular data type definitions. For example, whereas tree can represent trees
with any number of elements, the perfect type can only be used to represent
trees where the number of elements is a power of two.
The combination of type operators and polymorphism makes it possible to
encode non-regular types in System F𝜔. Here is a definition of a type corre-
sponding to perfect:
Perfect = 𝜆𝛼 : : ∗ .∀𝜑 : : ∗⇒∗ . ( ∀𝛼 : : ∗ .𝛼 → 𝜑 𝛼) →(∀𝛼 : : ∗ .𝜑 (𝛼 × 𝛼)→ 𝜑 𝛼)→ 𝜑 𝛼
As in our other examples, there is an argument corresponding to each con-
structor of the type. In order to capture the non-regularity of the original type
these arguments are themselves polymorphic functions.
The functions corresponding to ZeroP and SuccP follow the usual pattern,
except that we must instantiate the polymorphic function arguments when ap-
plying them:
zeroP = Λ𝛼 : : ∗ .𝜆x :𝛼 .
Λ𝜑 : : ∗⇒∗ .𝜆z :∀𝛼 : : ∗ .𝛼 → 𝜑 𝛼 .𝜆s :𝜑 (𝛼 × 𝛼)→ 𝜑 𝛼 . z [ ] x
succP = Λ𝛼 : : ∗ .𝜆p : Perfect (𝛼 × 𝛼) .
Λ𝜑 : : ∗⇒∗ .𝜆z :∀𝛼 : : ∗ .𝛼 → 𝜑 𝛼 .𝜆s : ( ∀𝛽 : : ∗ .𝜑 (𝛽 × 𝛽)→ 𝜑 𝛽) .
s [𝛼 ] (p [𝜑 ] z s )
We will have more to say about non-regular types in Chapter 8, since they
are fundamental to GADTs.
Encoding type equality in System F𝜔 Our final example encodes a rather
unusual data type which will also play a fundamental role in Chapter 8.
Perhaps you have encountered Leibniz’s definition of equality, which states
that objects should be considered equal if they behave identically in any context.
We can express this notion of equality for types within System F𝜔 as follows:
Eq = 𝜆𝛼 : : ∗ .𝜆𝛽 : : ∗ .∀𝜑 : : ∗⇒∗ .𝜑 𝛼 → 𝜑 𝛽
2.5. A NOTE ON THE LAMBDA CUBE AND DEPENDENT TYPES 27
That is, for any types 𝛼 and 𝛽 we can build a value Eq 𝛼 𝛽 if, for any unary
type operator 𝜑 we can convert from 𝜑 𝛼 to type 𝜑 𝛽. (It might be supposed
that we should also include the converse conversion 𝜑 𝛽 → 𝜑 ; we shall see in a
moment why it’s unnecessary to do so.)
Applying the Eq operator twice to any type 𝛼 gives us a type Eq 𝛼 𝛼, which
is inhabited by a polymorphic identity function. We call the inhabitant refl ,
since it represents the reflexivity of equality:
r e f l = Λ𝛼 : : ∗ .Λ𝜑 : : ∗⇒∗ .𝜆x :𝜑 𝛼 . x
Similarly we can define values of the following types to represent the sym-
metry and transitivity properties:
symm : ∀𝛼 : : ∗ .∀𝛽 : : ∗ .Eq 𝛼 𝛽 → Eq 𝛽 𝛼
trans : ∀𝛼 : : ∗ .∀𝛽 : : ∗ .∀𝛾 : : ∗ .Eq 𝛼 𝛽 → Eq 𝛽 𝛾 → Eq 𝛼 𝛾
Here are the definitions:
symm = Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .𝜆e : ( ∀𝜑 : : ∗⇒∗ .𝜑 𝛼 → 𝜑 𝛽) . e [𝜆𝛾 : : ∗ .Eq 𝛾 𝛼 ] ( r e f l [𝛼 ] )
trans = Λ𝛼 : : ∗ .Λ𝛽 : : ∗ .Λ𝛾 : : ∗ .𝜆ab :Eq 𝛼 𝛽 .𝜆bc :Eq 𝛽 𝛾 . bc [Eq 𝛼 ] ab
Finally, we can define a function lift whose type tells us that if two types 𝛼
and 𝛽 are equal then 𝜑 𝛼 and 𝜑 𝛽 are also equal, for any 𝜑:
lift : ∀𝛼 : : ∗ .∀𝛽 : : ∗ .∀𝜑 : : ∗⇒∗ .Eq 𝛼 𝛽 → Eq (𝜑 𝛼) (𝜑 𝛽)
Here is the definition of lift :
lift = Λ𝛼 : : ∗ .
Λ𝛽 : : ∗ .
Λ𝜑 : : ∗⇒∗ .
𝜆e :Eq 𝛼 𝛽 .
e [𝜆𝛾 : : ∗ .Eq (𝜑 𝛼) (𝜑 𝛾 ) ] ( r e f l [𝜑 𝛼 ] )
Kind polymorphism As the notation for type-level abstraction suggests,
System F𝜔 enriches System F with what amounts to a simply-typed lambda
calculus at the type level. This observation suggests ways that we might further
extend the abstraction facilities of the calculus — for example, we might add
type-level polymorphism over kinds in the same way that we added term-level
polymorphism over types. Polymorphism over kinds would allow us to generalize
our definition of equality to arbitrary type operators.
2.5 A note on the lambda cube and dependent
types
Dependent types In this chapter we’ve seen three different forms of abstrac-
tion:
• The first calculus, 𝜆→ (Section 2.2), supports “term-to-term” abstraction.
The →-intro rule allows us to build terms 𝜆x:A.M denoting functions that
abstract over terms.
28 CHAPTER 2. LAMBDA CALCULUS
• The second calculus, System F (Section 2.3) adds support for “type-to-
term” abstraction. The ∀-intro rule allows us to build terms Λ𝛼::K.M that
abstract over types.
• The final calculus, System F𝜔 (Section 2.4) adds support for “type-to-
type” abstraction. The ⇒-intro rule allows us to build types (or, more
precisely, type-expressions) 𝜆𝛼::K.A that abstract over types (strictly: type
expressions).
At this point the question naturally arises: might there be a calculus which
supports “term-to-type” abstraction? The (affirmative) answer comes in the
form of a richly expressive set of “dependently typed” calculi. Dependent types
form the basis of many tools used in computer assisted theorem proving (such
as Coq9 and Twelf10) and are increasingly making their way into practical pro-
gramming languages such as Idris, Agda, and GHC Haskell. Dependent types
are beyond the scope of this course, but we’ll note in passing how the extra power
they offer comes in handy when we look at Propositions as Types (Chapter 4)
and Generalised Algebraic Data Types (Chapter 8).
The lambda cube We’ve presented the route from 𝜆→ to System F to Sys-
tem F𝜔 as a natural, almost inevitable progression. However, type-level abstrac-
tion and polymorphism are sufficiently independent that we could equally well
have introduced them in the opposite order. In fact, the three ways of extend-
ing 𝜆→ with additional forms of abstraction can be applied in any combination,
leading to a collection of eight different calculi. This is sometimes visualised as a
cube with 𝜆→ at one corner and (a version of) the calculus of constructions 𝑃𝜔,
which supports all four forms of abstraction, in the farthest corner, as shown
in Figure 2.4. The three systems (𝜆→, System F, and System F𝜔) that we’ve
considered in this chapter all lie on the left face.
2.6 Exercises
1. [H]: Give a typing derivation for swap
2. [HH]: We have seen how to implement booleans in System F using sums
and the unit type. Give an equivalent implementation of booleans using
polymorphism, using ℕ encoding as an example.
3. [HHH]: Implement a signed integer type, either using booleans, products
and ℕ, or directly in System F. Give an addition function for your signed
integers.
4. [HH]: Show how to encode the tree type in System F𝜔.
9https://coq.inria.fr/
10http://twelf.org/
https://coq.inria.fr/
http://twelf.org/
2.6. EXERCISES 29
𝜆𝜔 𝜆𝐶
𝜆2
��������
𝜆𝑃2
��������
𝜆𝜔 𝜆𝑃𝜔
𝜆→
�������
𝜆𝑃
��������
Figure 2.4: The “lambda cube”
terms on types
OO�
�
�
�
�
�
�
�
�
�
types on terms
//__________
types on types
??�
�
�
�
�
�
�
Figure 2.5: Dependencies in the
lambda cube
Key
• 𝜆→: simply typed lambda calculus (Section 2.2)
• 𝜆2: System F (Section 2.3)
• 𝜆𝜔: System F𝜔 (Section 2.4)
5. [HH]: Write a function that computes the sum of a list of natural numbers
in System F𝜔.
6. [H]: Give an encoding of OCaml’s option type in System F𝜔:
type ’ a option =
None : ’ a option
| Some : ’ a -> ’a option
7. [HHH]: Use existentials, the list type, the product type, the ℕ encod-
ing and your option type from question 6 to implement a stack interface
corresponding to the following OCaml signature:
type ’ a t
val empty : ’ a t
val push : ’ a -> ’a t -> ’a t
val pop : ’ a t -> ’a option * ’a t
val s i z e : ’ a t -> int
30 CHAPTER 2. LAMBDA CALCULUS
These notes aim to be self-contained, but fairly terse. There are many
more comprehensive introductions to the typed lambda calculi available.
The following two books are highly recommended:
• Types and Programming Languages
Benjamin C. Pierce
MIT Press (2002)
http://www.cis.upenn.edu/~bcpierce/tapl/
There are copies in the Computer Laboratory library and many of the
college libraries.
• Lambda Calculi with Types
Henk Barendregt
in Handbook of Logic in Computer Science Volume II, Oxford Uni-
versity Press (1992)
Available online: http://ttic.uchicago.edu/~dreyer/course/papers/
barendregt.pdf
http://www.cis.upenn.edu/~bcpierce/tapl/
http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf
http://ttic.uchicago.edu/~dreyer/course/papers/barendregt.pdf