Contents
Learning Guide i
1 Introduction 1
2 ML Polymorphism 6
2.1 Mini-ML type system . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
2.2 Examples of type inference, by hand . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2.3 Principal type schemes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
2.4 A type inference algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
3 Polymorphic Reference Types 25
3.1 The problem . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25
3.2 Restoring type soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
4 Polymorphic Lambda Calculus 33
4.1 From type schemes to polymorphic types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
4.2 The Polymorphic Lambda Calculus (PLC) type system . . . . . . . . . . . . . . . . . . . . 37
4.3 PLC type inference . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
4.4 Datatypes in PLC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
4.5 Existential types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
5 Dependent Types 53
5.1 Dependent functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
5.2 Pure Type Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
5.3 System Fw . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63
6 Propositions as Types 67
6.1 Intuitionistic logics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
6.2 Curry-Howard correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
6.3 Calculus of Constructions, lC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
6.4 Inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76
7 Further Topics 81
References 84
1 INTRODUCTION 1
1 Introduction
“One of the most helpful concepts in the whole of programming is the
notion of type, used to classify the kinds of object which are
manipulated. A significant proportion of programming mistakes are
detected by an implementation which does type-checking before it runs
any program. Types provide a taxonomy which helps people to think and
to communicate about programs.”
R. Milner, Computing Tomorrow (CUP, 1996), p264
“The fact that companies such as Microsoft, Google and Mozilla are
investing heavily in systems programming languages with stronger type
systems is not accidental – it is the result of decades of experience
building and deploying complex systems written in languages with weak
type systems.”
T. Ball and B. Zorn, Teach Foundational Language Principles,
Viewpoints, Comm. ACM (2014) 58(5) 30–31
Slide 1
This short course is primarily about the use of types in programming languages. Types also
play an important role in logic and specification languages; indeed the concept of type in the
sense we use it here first arose in the work of Russell (1903) as a way of avoiding certain
paradoxes in the logical foundations of mathematics. In a similar way, one can use types to
rule out paradoxical, non-sensical, or badly-behaved programs. We will return to the interplay
between types in programming languages and types in logic in the last part of this course
(Section 6).
Many programming language systems use types (and related notions such as structures,
classes, interfaces, etc.) to classify expressions according to their structure (e.g. ”this expres-
sion is an array of character strings”) and/or behaviour (e.g. ”this function takes an integer
argument and returns a list of booleans”). Opinions differ about the extent to which it is a
Good Thing for a programming language design to force users to specify typing information.
Slide 1 contains a couple of quotes from the pro camp (of which I am a member), one from the
previous century from the father of the ML family of languages and one more recent one from
a couple of senior researchers at Microsoft Research (whose article is subtitled “Industry is
ready and waiting for more graduates educated in the principles of programming languages”
– amen to that). What I think is indisputable is that type systems have been, and continue to
be, one of the most important channels by which developments in theoretical computer science
get applied in programming language design and software verification.
1 INTRODUCTION 2
Uses of type systems
I Detecting errors via type-checking, either statically
(decidable errors detected before programs are executed) or
dynamically (typing errors detected during program
execution).
I Abstraction and support for structuring large systems.
I Documentation.
I E�ciency.
I Whole-language safety.
Slide 2
Here are some ways (summarised on Slide 2) in which type systems for programming
languages get used:
Detecting errors Experience suggests that a significant proportion of programming mistakes
(such as trying to divide an integer by a string) can be detected by an implementation which
does static type-checking, i.e. which checks for typing errors before it runs any program. Type
systems used to implement such checks at compile-time necessarily involve decidable proper-
ties of program phrases, since otherwise the process of compilation is not guaranteed to ter-
minate. (Recall the notion of (algorithmic) decidability from the CST IB ‘Computation Theory’
course.) For example, in a Turing-powerful language (one that can code all recursive partial
functions), it is undecidable whether an arbitrary arithmetic expression evaluates to 0 or not;
hence static type-checking will not be able to eliminate all ‘division by zero’ errors. Of course
the more properties of program phrases a type systems can express the better and the devel-
opment of the subject is partly a search for greater expressivity; but expressivity is constrained
in theory by this decidability requirement, and is constrained in practice by questions of com-
putational feasibility and user comprehension.
Abstraction and support for structuring large systems Type information is a crucial part
of interfaces for modules and classes, allowing the whole to be to be designed independently
of particular implementations of its parts. Type systems form the backbone of various mod-
ule languages in which modules (‘structures’) are assigned types which are interfaces (‘signa-
tures’).
Documentation Type information in procedure/function declarations and in module/class
interfaces are a form of documentation, giving useful hints about intended use and behaviour.
Static type-checking ensures that this kind of ‘formal documentation’ keeps in step with changes
to the program.
1 INTRODUCTION 3
Efficiency Typing information can be used by compilers to produce more efficient code. For
example the first use of types in computer science (in the 1950s) was to improve the efficiency
of numerical calculations in Fortran by distinguishing between integer and real-value expres-
sions. Many static analyses carried out by optimising compilers make use of specialised type
systems; an example is the ‘region inference’ used in the ML Kit Compiler to replace much
garbage collection in the heap by stack-based memory management Tofte and Talpin (1997).
Whole-language safety A programming language is sometimes called safe if its programs
may have trapped errors (one that can be handled gracefully), but cannot have untrapped er-
rors (ones that cause unpredictable crashes). Type systems are an important tool for designing
safe languages, but in principle, an untyped language could be safe by virtue of performing
certain checks at run-time. Since such checks generally hamper efficiency, in practice very
few untyped languages are safe; Cardelli (1997) cites LISP as an example of an untyped, safe
language (and assembly language as the quintessential untyped, unsafe language). Although
typed languages may use a combination of run- and compile-time checks to ensure safety, they
usually emphasise the latter. In other words the ideal is to have a type system implementing
algorithmically decidable checks used at compile-time to rule out all untrapped run-time er-
rors (and some kinds of trapped ones as well). Of course some languages (such as C) employ
types without any pretensions to safety (via the use of casting and void).
Formal type systems
I Constitute the precise, mathematical characterisation of
informal type systems (such as occur in the manuals of most
typed languages.)
I Basis for type soundness theorems: “any well-typed program
cannot produce run-time errors (of some specified kind).”
I Can decouple specification of typing aspects of a language
from algorithmic concerns: the formal type system can define
typing independently of particular implementations of
type-checking algorithms.
Slide 3
Some languages are designed to be safe by virtue of a type system, but turn out not to
be—because of unforeseen or unintended uses of certain combinations of their features (object-
oriented languages seem particularly prone to this problem). We will see an example of this in
Section 3, where we consider the combination of ML polymorphism with mutable references.
Such difficulties have been a great spur to the development of the formal mathematics and
logic of type systems: one can only prove that a language is safe after its syntax and operational
semantics have been formally specified. Standard ML Milner et al. (1997) is the shining ex-
ample of a full-scale language possessing a complete such specification and whose type sound-
ness/safety (Slide 3) has been subject to proof. In this course we will look at smaller examples of
1 INTRODUCTION 4
formally specified type systems. To do so, we use the techniques introduced in the CST Part IB
course on Semantics of Programming Languages: to specify a formal type system one gives a
number of axioms and rules for inductively generating typing judgements, a typical example
of which is shown on Slide 4. Ideally the rules follow the structure of the phrases, explaining
how to type them in terms of how their subphrases can be typed – one speaks of syntax-directed
sets of rules. It is worth pointing out that different language families use different notations
for the has-type relation (Slide 5).
Typical type system judgement
is a relation between typing environments (G), program phrases (e)
and type expressions (t) that we write as
G ` e : t
and read as: given the assignment of types to free identifiers of e
specified by type environment G, then e has type t.
E.g.
f : int list � int, b : bool ` (if b then f nil else 3) : int
is a valid typing judgement about ML.
We consider structural type systems, in which there is a language
of type expressions built up using type constructs (e.g.
int list � int in ML).
(By contrast, in nominal type systems, type expressions are just
unstructured names.)
Slide 4
Notations for the typing relation
‘foo has type bar’
ML-style (used in this course):
foo : bar
Haskell-style:
foo :: bar
C/Java-style:
bar foo
Slide 5
1 INTRODUCTION 5
Once we have formalised a particular type system, we are in a position to prove results
about type soundness (Slide 3) and the notions of type checking, typeability and type inference de-
scribed on Slide 6. You have already seen some examples in the CST IB Semantics of Program-
ming Languages course of formal type systems defined using inductive definitions generated by
syntax-directed axioms and rules, together with progress, type-preservation and safety theorems
(Slide 7). In this course we will look at more involved examples revolving around the notions
of parametric polymorphism (Sections 2–4) and dependent functions (Sections 5 and 6).
Type checking, typeability, and type inference
Suppose given a type system for a programming language with
judgements of the form G ` e : t.
I Type-checking problem: given G, e, and t, is G ` e : t
derivable in the type system?
I Typeability problem: given G and e, is there any t for which
G ` e : t is derivable in the type system?
Solving the second problem usually involves devising a type
inference algorithm computing a t for each G and e (or failing, if
there is none).
Slide 6
Progress, type preservation & safety
Recall that the simple, typed imperative language considered in
CST Part IB Semantics of Programming Languages satisfies:
Progress. If G ` e : t and dom(G) ✓ dom(s), then either e is a
value, or there exist e0, s0 such that he, si ! he0, s0i.
Type preservation. If G ` e : t and dom(G) ✓ dom(s) and
he, si ! he0, s0i, then G ` e0 : t and dom(G) ✓ dom(s0).
Hence well-typed programs don’t get stuck:
Safety. If G ` e : t, dom(G) ✓ dom(s) and he, si !⇤ he0, s0i,
then either e0 is a value, or there exist e00, s00 such that
he0, s0i ! he00, s00i.
Slide 7
2 ML POLYMORPHISM 6
2 ML Polymorphism
As indicated in the Introduction, static type-checking is regarded by many as an important
aid to building large, well-structured, and reliable software systems. On the other hand, early
forms of static typing, for example as found in Pascal, tended to hamper the ability to write
generic code. For example, a procedure for sorting lists of one type of data could not be applied
to lists of a different type of data. It is natural to want a polymorphic sorting procedure—one
which operates (uniformly) on lists of several different types. The potential significance for
programming languages of this phenomenon of polymorphism was first emphasised by Stra-
chey (1967), who identified several different varieties: see Slide 8. Here we will concentrate on
parametric polymorphism, also known as generics.
One way to get parametric polymorphism is to make the type parameterisation an explicit
part of the language syntax: we will see an example of this in Section 4. In this section, we
look at the implicit version of parametric polymorphism first implemented in the ML family
of languages and subsequently adopted elsewhere, for example in Haskell, Java and C#. ML
phrases need contain no explicit type information: the type inference algorithm infers a most
general type (scheme) for each well-formed phrase, from which all the other types of the phrase
can be obtained by specialising type variables. These ideas should be familiar to you from your
previous experience of Standard ML. The point of this section is to see how one gives a math-
ematically precise formalisation of a type system and its associated type inference algorithm
for a small fragment of ML, called Mini-ML.
Polymorphism = has many types
I Overloading (or ad hoc polymorphism): same symbol
denotes operations with unrelated implementations. (E.g. +
might mean both integer addition and string concatenation.)
I Subsumption: subtyping relation t1 <: t2 allows any
M1 : t1 to be used as M1 : t2 without violating safety.
I Parametric polymorphism (generics): same expression
belongs to a family of structurally related types.
E.g. in Standard ML, length function
fun length nil = 0
| length (x :: xs) = 1 + (length xs)
has type t list � int for all types t.
Slide 8
2.1 Mini-ML type system
As indicated on Slide 9, to formalise parametric polymorphism, we introduce type variables. An
interactive ML system will just display a list � int as the type of the length function (Slide 8),
leaving the universal quantification over a implicit. However, when it comes to formalising
the ML type system (Milner et al., 1997, chapter 4)) it is necessary to make this universal quan-
tification over types explicit in some way. The reason for this has to do with the typing of local
2 ML POLYMORPHISM 7
declarations. Consider the example on Slide 10. The expression ( f true) :: ( f nil) has type
bool list, given some assumption about the type of the variable f . Two possible such forms of
assumption are shown on Slide 11. Here we are interested in the second possibility since it
leads to a type system with very useful properties. The form of Mini-ML typing judgements
is shown on Slide 12. The particular grammar of types and type schemes that we will use for
Mini-ML is shown on Slide 13.
Type variables and type schemes in Mini-ML
To formalise statements like
“length has type t list � int, for all types t”
we introduce type variables a (i.e. variables for which types may
be substituted) and write
length : 8a (a list � int).
8a (a list � int) is an example of a type scheme.
Slide 9
Polymorphism of let-bound variables in ML
For example in
let f = lx (x) in ( f true) :: ( f nil)
lx (x) has type t � t for any type t, and the variable f to which
it is bound is used polymorphically:
in ( f true), f has type bool � bool
in ( f nil), f has type bool list � bool list
Overall, the expression has type bool list.
Slide 10
2 ML POLYMORPHISM 8
Forms of hypothesis in typing judgements
I
Ad hoc (overloading):
if f : bool � bool
and f : bool list � bool list,
then ( f true) :: ( f nil) : bool list.
Appropriate for expressions that have di�erent behaviour at
di�erent types.
I
Parametric:
if f : 8a (a � a),
then ( f true) :: ( f nil) : bool list.
Appropriate if expression behaviour is uniform for di�erent
type instantiations.
ML uses parametric hypotheses (type schemes) in its typing
judgements.
Slide 11
Mini-ML typing judgement
takes the form
G ` M : t
where
I the typing environment G is a finite function from variables
to type schemes.
(We write G = {x1 : s1, . . . , xn : sn} to indicate that G has domain
of definition dom(G) = {x1, . . . , xn} (mutually distinct variables)
and maps each xi to the type scheme si for i = 1 . . . n.)
I M is a Mini-ML expression
I t is a Mini-ML type.
Slide 12
2 ML POLYMORPHISM 9
Mini-ML types and type schemes
Types t ::= a type variable
| bool type of booleans
| t � t function type
| t list list type
where a ranges over a fixed, countably infinite set TyVar.
Type Schemes s ::= 8A (t)
where A ranges over finite subsets of the set TyVar.
When A = {a1, . . . , an} (mutually distinct type variables) we write
8A (t) as
8a1, . . . , an (t).
When A = {} is empty, we write 8A (t) just as t. In other words,
we regard the set of types as a subset of the set of type schemes
by identifying the type t with the type scheme 8{ } (t).
Slide 13
The following points about type schemes 8A (t) should be noted.
(i) The case when A is empty, A = { }, is allowed: 8{ } (t) is a well-formed type scheme. We
will often regard the set of types as a subset of the set of type schemes by identifying
the type t with the type scheme 8{ } (t).
(ii) Any occurrences in t of a type variable a 2 A become bound in 8A (t). Thus by def-
inition, the free type variables of a type scheme 8A (t) are all those type variables which
occur in t, but which are not in the finite set A. (For example the set of free type variables
of 8a (a � a0) is {a0}.) We call a type scheme 8A (t) closed if it has no free type variables,
that is, if A contains all the type variables occurring in t. As usual for variable-binding
constructs, we are not interested in the particular names of 8-bound type variables (since
we may have to change them to avoid variable capture during substitution of types for
free type variables). Therefore we will identify type schemes up to alpha-conversion of
8-bound type variables. For example, 8a (a � a0) and 8a00 (a00 � a0) determine the same
alpha-equivalence class and will be used interchangeably. Of course the finite set
ftv(8A (t))
of free type variables of a type scheme is well-defined up to alpha-conversion of bound
type variables. Since we identify Mini-ML types t with trivial type schemes 8{ } (t), so
we sometimes write
ftv(t)
for the finite set of type variables occurring in t (of course all such occurrences are free,
because Mini-ML types do not involve binding operations).
(iii) ML type schemes cannot be used where an ML type is expected. So for example, a �
8a0 (a0) is neither a well-formed Mini-ML type nor a well-formed Mini-ML type scheme.1
Rather, Mini-ML type schemes are a notation for families of types, parameterised by type
variables. We get types from type schemes by substituting types for type variables, as we
explain next.
1The step of making type schemes first class types will be taken in Section 4.
2 ML POLYMORPHISM 10
Specialising type schemes to types
A type t is a specialisation of a type scheme
s = 8a1, . . . , an (t0) if t can be obtained from the type t0 by
simultaneously substituting some types ti for the type variables ai
(i = 1, . . . , n):
t = t0[t1/a1, . . . , tn/an]
In this case we write s � t
(N.B. The relation is una�ected by the particular choice of names of
bound type variables in s.)
The converse relation is called generalisation: a type scheme s
generalises a type t if s � t.
Slide 14
Slide 14 gives some terminology and notation to do with substituting types for the bound
type variables of a type scheme. The notion of a type scheme generalising a type will feature in
the way variables are assigned types in the Mini-ML type system that we are going to define
in this section.
Example 1. Some simple examples of specialising type schemes:
8a (a � a) � bool � bool
8a (a � a) � a0 list � a0 list
8a (a � a) � (a0 � a0)� (a0 � a0).
However
8a (a � a) ⌥ (a0 � a0)� a0.
This is because in a substitution t[t0/a], by definition we have to replace all occurrences in t of
the type variable a by t0. Thus when t = a � a, there is no type t0 for which t[t0/a] is the type
(a � a) � a. (Simply because in the syntax tree of t[t0/a] = t0 � t0, the two subtrees below
the outermost constructor ‘�’ are equal (namely to t0), whereas this is false of (a � a) � a.)
Another example:
8a1, a2 (a1 � a2) � a list � bool.
However
8a1 (a1 � a2) ⌥ a list � bool
because a2 is a free type variable in the type scheme 8a1 (a1 � a2) and so cannot be substituted
for during specialisation.
2 ML POLYMORPHISM 11
Mini-ML expressions
M ::= x variable
| true boolean values
| false
| if M then M else M conditional
| lx (M) function abstraction
| M M function application
| let x = M in M local declaration
| nil nil list
| M :: M list cons
| case M of nil ) M | x :: x ) M case expression
Slide 15
Just as we only consider a small subset of ML types, for Mini-ML we restrict attention to
typings for a small subset of ML expressions, M, generated by the grammar on Slide 15. We
use a non-standard syntax compared with the definition in Milner et al. (1997). For example
we write lx (M) for fn x => M and let x = M1 in M2 for let val x = M1 in M2 end. (Fur-
thermore we will call the symbol ‘x’ occurring in these expressions a variable rather than a
(value) identifier.) The axioms and rules inductively generating the Mini-ML typing relation for
these expressions are given on Slides 16–18. As usual, the axioms and rules on Slides 16–18 are
schematic: G stands for any type environment; x and ` for any variables; M, M1, M2, M3, L, N
and C for any expressions; and t, t0, t1 and t2 for any types.
Note the following points about the type system defined on Slides 16–18.
(i) As usual, any free occurrences of x in M become bound in lx (M). In the expression
let x = M1 in M2, any free occurrences of the variable x in M2 become bound in the
let-expression. Similarly, in the expression case M1 of nil) M2 | x1 :: x2) M3, any
free occurrences of the variables x1 and x2 in M3 become bound in the case-expression.
We identify expressions up to alpha-conversion of bound variables. For example,
let x = lx (x) in x x and let f = lx (x) in f f determine the same alpha-equivalence class
and will be used interchangeably.
(ii) Given a type environment G we write G, x : s to indicate a typing environment with
domain dom(G) [ {x}, mapping x to s and otherwise mapping like G. When we use this
notation it will almost always be the case that x /2 dom(G): cf. rules (fn), (let) and (case).
Note also that side conditions such as x /2 dom(G) in these rules can often be satisfied by
suitably renaming bound variables to be fresh (relying upon the previous point).
(iii) In rule (fn) we use G, x : t1 as an abbreviation for G, x : 8{ } (t1). Similarly, in rule (case),
G, x : t, ` : t list really means G, x : 8{ } (t), ` : 8{ } (t list). (Recall that by definition, a
typing environment has to map variables to type schemes, rather than to types.)
(iv) In rule (let) the notation ftv(G) means the set of all type variables occurring free in some
type scheme assigned in G. For example, if G = {x1 : s1, . . . , xn : sn}, then ftv(G) =
2 ML POLYMORPHISM 12
ftv(s1)[ · · ·[ ftv(sn). Thus the set A = ftv(t)� ftv(G) used in the rule consists of all type
variables in t that do not occur freely in any type scheme assigned in G. Slide 19 gives an
example instance of the (let) rule.
Mini-ML type system, I
(var �)
G ` x : t
if (x : s) 2 G and s � t
(bool)
G ` B : bool
if B 2 {true, false}
(if)
G ` M1 : bool G ` M2 : t G ` M3 : t
G ` (if M1 then M2 else M3) : t
Slide 16
Mini-ML type system, II
(nil)
G ` nil : t list
(cons)
G ` M : t G ` L : t list
G ` M :: L : t list
(case)
G ` L : t list G ` N : t0
G, x : t, ` : t list ` C : t0
G ` (case L of nil ) N | x :: `) C) : t0
if x 6= ` and
x, ` /2 dom(G)
Slide 17
2 ML POLYMORPHISM 13
Mini-ML type system, III
(fn)
G, x : t1 ` M : t2
G ` lx (M) : t1 � t2
if x /2 dom(G)
(app)
G ` M : t1 � t2 G ` N : t1
G ` M N : t2
(let)
G ` M1 : t
G, x : 8A (t) ` M2 : t0
G ` (let x = M1 in M2) : t0
if x /2 dom(G) and
A = ftv(t)� ftv(G)
Definition. We write G ` M : 8A (t) to mean G ` M : t is
derivable from the Mini-ML typing rules and that
A = ftv(t)� ftv(G).
(So (let) is equivalent to
G ` M1 : s G, x : s ` M2 : t0
G ` (let x = M1 in M2) : t0
if x /2 dom(G).)
Slide 18
Example of using the (let) rule
(let)
G ` M1 : t
G, x : 8A (t) ` M2 : t0
G ` (let x = M1 in M2) : t0
if x /2 dom(G) and
A = ftv(t)� ftv(G)
If G ` M1 : t is y : b, z : 8g (g � g � bool) ` lu (y) : a � b
then A = {a, b}� {b} = {a} and 8A (t) = 8a (a � b).
So if G, x : 8A (t) ` M2 : t0 is
y : b, z : 8g (g � g � bool), x : 8a (a � b) ` z (x y) (x nil) : bool
then applying (let) yields
y : b, z : 8g (g � g � bool) ` let x = lu (y) in z (x y) (x nil) : bool
Slide 19
The Mini-ML rules are used to inductively generate the typing relation. We say that G ` M :
8A (t) is derivable (or provable, or valid) in the type system if there is a proof of G ` M : t using
the axioms and rules and A = ftv(t)� ftv(G) (see the definition on Slide 18). When G = { } we
just write
` M : 8A (t) (1)
for { } ` M : 8A (t) and say that the (necessarily closed – see Exercise 2) expression M is
typeable in Mini-ML with type scheme 8A (t).
2 ML POLYMORPHISM 14
Example 2. We verify that the example of polymorphism of let-bound variables given on
Slide 10 has the type claimed there (and illustrate one style of setting out proofs of typing
– as a list of judgements successively derived by applying the rules; proof trees exhibit the
structure of typing proofs more clearly, but are less convenient to fit on a page!).
1. x : a ` x : a by (var), since 8{ } (a) � a.
2. { } ` lx (x) : a � a by (fn) on 1.
3. f : 8a (a � a) ` f : bool � bool by (var), since 8a (a � a) � bool � bool.
4. f : 8a (a � a) ` true : bool by (bool).
5. f : 8a (a � a) ` f true : bool by (app) on 3 and 4.
6. f : 8a (a � a) ` f : bool list � bool list by (var), since 8a (a � a) � bool list � bool list.
7. f : 8a (a � a) ` nil : bool list by (nil).
8. f : 8a (a � a) ` f nil : bool list by (app) on 6 and 7.
9. f : 8a (a � a) ` ( f true) :: ( f nil) : bool list by (cons) on 5 and 8.
10. { } ` let f = lx (x) in ( f true) :: ( f nil) : bool list by (let) on 2 and 9, since {a} = ftv(a �
a)� ftv({ }).
2.2 Examples of type inference, by hand
As for the full ML type system, for the type system we have just introduced the typeability
problem (Slide 6) turns out to be decidable. Moreover, among all the possible type schemes a
given closed Mini-ML expression may possess, there is a most general one—one from which
all the others can be obtained by substitution. Before showing why this is the case, we give
some specific examples of type inference in this type system.
Two examples involving self-application
M , let f = lx1 (lx2 (x1)) in f f
M0 , (l f ( f f )) lx1 (lx2 (x1))
Are M and M0 typeable in the Mini-ML type system?
Slide 20
2 ML POLYMORPHISM 15
(C3)
x1 : t3, x2 : t5 ` x1 : t6(C2)
x1 : t3 ` lx2 (x1) : t4
(C1)
{ } ` lx1 (lx2 (x1)) : t2
(C5)
f : 8A (t2) ` f : t7
(C6)
f : 8A (t2) ` f : t8
(C4)
f : 8A (t2) ` f f : t1
(C0)
{ } ` let f = lx1 (lx2 (x1)) in f f : t1
Figure 1: Skeleton proof tree for let f = lx1 (lx2 (x1)) in f f
Given a typing environment G and an expression M, how can we decide whether or not
there is a type scheme 8A (t) for which G ` M : 8A (t) holds? We are aided in this task by
the syntax-directed (or structural) nature of the axioms and rules: if G ` M : 8A (t) is derivable,
i.e. if A = ftv(t) � ftv(G) and G ` M : t is derivable from the rules on Slides 16–18, then
the outermost form of the expression M dictates which must be the last axiom or rule used
in the proof of G ` M : t. Consequently, as we try to build a proof of a typing judgement
G ` M : t from the bottom up, the structure of the expression M determines the shape of
the tree together with which rules are used at its nodes and which axioms at its leaves. For
example, for the particular expression M given on Slide 20, any proof of {} ` M : t1 from the
axioms and rules, has to look like the tree given in Figure 1. Node (C0) is supposed to be an
instance of the (let) rule; nodes (C1) and (C2) instances of the (fn) rule; leaves (C3), (C5), and
(C6) instances of the (var �) axiom; and node (C4) an instance of the (app) rule. For these to
be valid instances the constraints (C0)–(C6) listed on Slide 21 have to be satisfied.
Constraints generated while inferring a type for
let f = lx1 (lx2 (x1)) in f f
A = ftv(t2) (C0)
t2 = t3 � t4 (C1)
t4 = t5 � t6 (C2)
8{ } (t3) � t6, i.e. t3 = t6 (C3)
t7 = t8 � t1 (C4)
8A (t2) � t7 (C5)
8A (t2) � t8 (C6)
Slide 21
Thus M is typeable if and only if we can find types t1, . . . , t8 satisfying the constraints on
Slide 21. First note that they imply
t2
(C1)
= t3 � t4
(C2)
= t3 � (t5 � t6)
(C3)
= t6 � (t5 � t6).
So let us take t5, t6 to be type variables, say a2, a1 respectively. Hence by (C0), A = ftv(t2) =
2 ML POLYMORPHISM 16
ftv(a1 � (a2 � a1)) = {a1, a2}. Then (C4), (C5) and (C6) require that
8a1, a2 (a1 � (a2 � a1)) � t8 � t1 and 8a1, a2 (a1 � (a2 � a1)) � t8.
In other words there have to be some types t9, . . . , t12 such that
t9 � (t10 � t9) = t8 � t1 (C7)
t11 � (t12 � t11) = t8. (C8)
Now (C7) can only hold if
t9 = t8 and t10 � t9 = t1
and hence
t1 = t10 � t9 = t10 � t8
(C8)
= t10 � (t11 � (t12 � t11)).
with t10, t11, t12 otherwise unconstrained. So if we take them to be type variables a3, a4, a5
respectively, all in all, we can satisfy all the constraints on Slide 21 by defining
A = {a1, a2}
t1 = a3 � (a4 � (a5 � a4))
t2 = a1 � (a2 � a1)
t3 = a1
t4 = a2 � a1
t5 = a2
t6 = a1
t7 = (a4 � (a5 � a4))� (a3 � (a4 � (a5 � a4)))
t8 = a4 � (a5 � a4).
With these choices, Figure 1 becomes a valid proof of
{ } ` let f = lx1 (lx2 (x1)) in f f : a3 � (a4 � (a5 � a4))
from the typing axioms and rules on Slides 16–18, i.e. we do have
` let f = lx1 (lx2 (x1)) in f f : 8a3, a4, a5 (a3 � (a4 � (a5 � a4))) (2)
If we go through the same type inference process for the expression M0 on Slide 20 we
generate a tree and set of constraints as in Figure 2. These imply in particular that
t7
(C13)
= t4
(C12)
= t6
(C11)
= t7 � t5.
But there are no types t5, t7 satisfying t7 = t7 � t5, because t7 � t5 contains at least one more
‘�’ symbol than does t7. So we conclude that (l f ( f f )) lx1 (lx2 (x1)) is not typeable within
the ML type system.
2.3 Principal type schemes
The type scheme 8a3, a4, a5 (a3 � (a4 � (a5 � a4))) not only satisfies (2), it is in fact the most
general, or principal type scheme for let f = lx1 (lx2 (x1)) in f f , as defined on Slide 22. It is
worth pointing out that in the presence of (a), the converse of condition (b) on Slide 22 holds: if
` M : 8A (t) and 8A (t) � t0, then ` M : 8A0 (t0) (where A0 = ftv(t0)). This is a consequence
of the substitution property of valid Mini-ML typing judgements given in the Exercises.
Slide 23 gives the main result about the Mini-ML typeability problem. It was first proved
for a simple type system without polymorphic let-expressions by Hindley (1969) and ex-
tended to the full system by Damas and Milner (1982).
2 ML POLYMORPHISM 17
(C12)
f : t4 ` f : t6
(C13)
f : t4 ` f : t7
(C11)
f : t4 ` f f : t5
(C10)
{ } ` l f ( f f ) : t2
(C16)
x1 : t8, x2 : t10 ` x1 : t11(C15)
x1 : t8 ` lx2 (x1) : t9
(C14)
{ } `: lx1 (lx2 (x1)) : t3
(C9)
{ } ` (l f ( f f )) lx1 (lx2 (x1)) : t1
Constraints:
t2 = t3 � t1 (C9)
t2 = t4 � t5 (C10)
t6 = t7 � t5 (C11)
8{ } (t4) � t6, i.e. t4 = t6 (C12)
8{ } (t4) � t7, i.e. t4 = t7 (C13)
t3 = t8 � t9 (C14)
t9 = t10 � t11 (C15)
8{ } (t11) � t8, i.e. t11 = t8 (C16)
Figure 2: Skeleton proof tree and constraints for (l f ( f f )) lx1 (lx2 (x1))
Principal type schemes for closed expressions
A type scheme 8A (t) is the principal type scheme of a
closed Mini-ML expression M if
(a) ` M : 8A (t)
(b) for any other type scheme 8A0 (t0),
if ` M : 8A0 (t0), then 8A (t) � t0
Slide 22
Remark 3 (Complexity of the type checking algorithm). Although typeability is decidable,
it is known to be exponential-time complete. Furthermore, the principal type scheme of an
expression can be exponentially larger than the expression itself, even if the type involved
is represented efficiently as a directed acyclic graph. More precisely, in the worst case the
time taken to decide typeability and the space needed to display the principal type are both
exponential in the number of nested let’s in the expression. For example the expression on
Slide 24 (taken from Mairson (1990)) has a principal type scheme which would take hundreds
of pages to print out. It seems that such pathology does not arise naturally, and that the type
checking phase of an ML compiler is not a bottle neck in practice. For more details about the
2 ML POLYMORPHISM 18
complexity of ML type inference see (Mitchell, 1996, Section 11.3.5).
Theorem (Hindley; Damas-Milner)
Theorem. If the closed Mini-ML expression M is typeable (i.e.
` M : s holds for some type scheme s), then there is a principal
type scheme for M.
Indeed, there is an algorithm which, given any closed Mini-ML
expression M as input, decides whether or not it is typeable and
returns a principal type scheme if it is.
Slide 23
An ML expression with
a principal type scheme
hundreds of pages long
let pair = lx (ly (lz (z x y))) in
let x1 = ly (pair y y) in
let x2 = ly (x1(x1 y)) in
let x3 = ly (x2(x2 y)) in
let x4 = ly (x3(x3 y)) in
let x5 = ly (x4(x4 y)) in
x5(ly (y))
Slide 24
2.4 A type inference algorithm
The aim of this subsection is to sketch the proof of the Hindley-Damas-Milner theorem stated
on Slide 23, by describing an algorithm, pt, for deciding typeability and returning a most gen-
2 ML POLYMORPHISM 19
eral type scheme. pt is defined recursively, following structure of expressions (and its termina-
tion is proved by induction on the structure of expressions).
As the examples in Section 2.2 suggest, the algorithm depends crucially upon unification—
the fact that the solvability of a finite set of equations between algebraic terms is decidable and
that a most general solution exists, if any does. This fact was discovered by Robinson (1965)
and has been a key ingredient in several logic-related areas of computer science (automated
theorem proving, logic programming, and of course type systems, to name three). The form of
unification algorithm, mgu, we need here is specified on Slide 25. Although we won’t bother
to give an implementation of mgu here (see for example (Rydeheard and Burstall, 1988, Chap-
ter 8), (Mitchell, 1996, Section 11.2.2), or (Aho et al., 1986, Section 6.7) for more details), we do
need to explain the notation for type substitutions introduced on Slide 25.
Unification of ML types
There is an algorithm mgu which when input two Mini-ML types
t1 and t2 decides whether t1 and t2 are unifiable, i.e. whether
there exists a type-substitution S 2 Sub with
(a) S(t1) = S(t2).
Moreover, if they are unifiable, mgu(t1, t2) returns the most
general unifier—an S satisfying both (a) and
(b) for all S0 2 Sub, if S0(t1) = S0(t2), then S0 = TS for some
T 2 Sub
(any other substitution S0 can be factored through
S, by specialising S with T)
By convention mgu(t1, t2) = FAIL if (and only if) t1 and t2 are not
unifiable.
Slide 25
Definition 4 (Type substitutions). A type substitution S is a (totally defined) function from type
variables to Mini-ML types with the property that S(a) = a for all but finitely many a. We write
Sub for the set of all such functions. The domain of S 2 Sub is the finite set of variables
dom(S) , {a 2 TyVar | S(a) 6= a}
Given a type substitution S, the effect of applying the substitution to a type is written S t;
thus if dom(S) = {a1, . . . , an} and S(ai) is the type ti for each i = 1..n, then S(t) is the type
resulting from simultaneously replacing each occurrence of ai in t with ti (for all i = 1..n), i.e.
S t = t[t1/a1, . . . , tn/an]
using the notation for substitution from Slide 14. Notwithstanding the notation on the right
hand side of the above equation, we prefer to write the application of a type substitution func-
tion S on the left of the type to which it is being applied.2 As a result, the composition TS of
two type substitutions S, T 2 Sub means first apply S and then T. Thus by definition TS is
2i.e. we write S t rather than t S as in the Part IB Logic and Proof course.
2 ML POLYMORPHISM 20
the function mapping each type variable a to the type T(S(a)) (apply the type substitution T
to the type S(a)). Note that the function TS does satisfy the finiteness condition required of a
substitution and we do have TS 2 Sub; indeed, dom(TS) ✓ dom(T) [ dom(S).
More generally, if dom(S) = {a1, . . . , an} and s is a Mini-ML type scheme, then S s will
denote the result of the (capture-avoiding3) substitution of S(ai) for each free occurrence of ai
in s (for i = 1..n).
Even though we are ultimately interested in the typeability of closed expressions, since
the algorithm pt descends recursively through the subexpressions of the input expression, in-
evitably it has to generate typings for expressions with free variables. Hence we have to define
the notions of typeability and principal type scheme for open expressions in the presence of a
non-empty typing environment. This is done on Slide 26. For the definitions on that slide to be
reasonable, we need some properties of the typing relation with respect to type substitutions
and specialisation. These are stated on Slide 28; we leave the proofs as exercises. To com-
pute principal type schemes it suffices to compute principal solutions in the sense of Slide 26.
(Slide 27 illustrates this notion of a solution to a typing problem.) For if M is in fact closed, then
any principal solution (S, s) for the typing problem { } ` M : ? has the property that s is a
principal type scheme for M in the sense of Slide 22 (see the exercises).
Principal type schemes for open expressions
A solution for the typing problem G ` M : ? is a pair (S, s)
consisting of a type substitution S and a type scheme s satisfying
S G ` M : s
(where S G = {x1 : S s1, . . . , xn : S sn}, if G = {x1 : s1, . . . , xn : sn}).
Such a solution is principal if given any other, (S0, s0), there is
some T 2 Sub with TS = S0 and T(s) � s0.
(For type schemes s and s0, with s0 = 8A0 (t0) say, we define
s � s0 to mean A0 \ ftv(s) = {} and s � t0.)
Slide 26
3Since we identify type schemes up to renaming their 8-bound type variables, we always assume the bound
type variables in s are different from any type variables in the types S(ai).
2 ML POLYMORPHISM 21
Example typing problem and solutions
Typing problem
x : 8a (b � (g � a)) ` x true : ?
has solutions:
I S1 = {b 7! bool}, s1 = 8a (g � a)
I S2 = {b 7! bool, g 7! a}, s2 = 8a0 (a � a0)
I S3 = {b 7! bool, g 7! a}, s3 = 8a0 (a � (a0 � a0))
I S4 = {b 7! bool, g 7! bool}, s3 = 8{ } (bool � bool)
Both (S1, s1) and (S2, s2) are in fact principal solutions.
Slide 27
Properties of the Mini-ML typing relation
with respect to substitution
and type scheme specialisation
I If G ` M : s, then for any type substitution S 2 Sub
SG ` M : Ss
I If G ` M : s and s � s0, then
G ` M : s0
Slide 28
2 ML POLYMORPHISM 22
Requirements for a
principal typing algorithm, pt
pt operates on typing problems G ` M : ? (consisting of a typing
environment G and a Mini-ML expression M).
It returns either a pair (S, t) consisting of a type substitution
S 2 Sub and a Mini-ML type t, or the exception FAIL.
I If G ` M : ? has a solution (cf. Slide 28), then pt(G ` M : ?)
returns (S, t) for some S and t;
moreover, setting A = (ftv(t)� ftv(S G)), then
(S,8A (t)) is a principal solution for the problem G ` M : ?.
I If G ` M : ? has no solution, then pt(G ` M : ?) returns
FAIL.
Slide 29
How the principal typing algorithm pt works
pt(G ` M : ?) = (S, t) | FAIL
I Call pt recursively following the structure of M and guided by
the typing rules, bottom-up.
I Thread substitutions sequentially and compose them together
when returning from a recursive call.
I When types need to agree to satisfy a typing rule, use mgu
(and pt returns FAIL only if mgu does).
I When types are unknown, generate a fresh type variable.
Slide 30
2 ML POLYMORPHISM 23
• Variables: pt(G ` x : ?) , let 8A (t) = G(x) in (Id, t)
• let-Expressions: pt(G ` let x = M1 in M2 : ?) ,
let (S1, t1) = pt(G ` M1 : ?) in
let A = ftv(t1)� ftv(S1 G) in
let (S2, t2) = pt(S1G, x : 8A (t1) ` M2 : ?) in (S2S1, t2)
• Booleans (B = true, false): pt(G ` B : ?) , (Id, bool)
• Conditionals: pt(G ` if M1 then M2 else M3 : ?) ,
let (S1, t1) = pt(G ` M1 : ?) in
let S2 = mgu(t1, bool) in
let (S3, t3) = pt(S2S1 G ` M2 : ?) in
let (S4, t4) = pt(S3S2S1 G ` M3 : ?) in
let S5 = mgu(S4 t3, t4) in (S5S4S3S2S1, S5 t4)
Figure 3: Some of the clauses in a definition of pt
Some of the clauses in a definition of pt
Function abstractions: pt(G ` lx (M) : ?) ,
let a = fresh in
let (S, t) = pt(G, x : a ` M : ?) in (S, S(a)�t)
Function applications: pt(G ` M1 M2 : ?) ,
let (S1, t1) = pt(G ` M1 : ?) in
let (S2, t2) = pt(S1 G ` M2 : ?) in
let a = fresh in
let S3 = mgu(S2 t1, t2 � a) in (S3S2S1, S3(a))
Slide 31
Slide 29 specifies what is required of the principal typing algorithm, pt; and Slide 30 in-
dicates, in general terms, how to meet the specification. One possible implementation, writ-
ten in somewhat informal pseudocode (and leaving out the cases for nil, cons, and case-
expressions), is sketched on Slide 31 and in Figure 3.4 Note the following points about the
definitions on Slide 31 and in Figure 3:
(i) We implicitly assume that all bound variables in expressions and bound type variables
in type schemes are distinct from each other and from any other variables in context. So,
for example, the clause for function abstractions tacitly assumes that x /2 dom(G); and the
clause for variables assumes that A \ ftv(G) = { }.
4An implementation in Fresh OCaml (www.cl.cam.ac.uk/users/amp12/fresh-ocaml/) can be found on the
course web page. The Fresh OCaml code is remarkably close to the informal pseudocode given here, because of
Fresh OCaml’s facilities for dealing with binding operations and fresh names.
2 ML POLYMORPHISM 24
(ii) The type substitution Id occurring in the clauses for variables and booleans is the identity
substitution which maps each type variable a to itself.
(iii) The clauses of the definition for nil, cons, and case-expressions are left as exercises.
(iv) We do not give the proof that the definition in Figure 3 is correct (i.e. meets the specifica-
tion on Slide 29). The correctness of the algorithm depends upon an important property
of Mini-ML typing, namely that it is respected by the operation of substituting types for type
variables.
More efficient algorithms make use of a different approach to substitution and unifica-
tion, based on equivalence relations on directed acyclic graphs and union-find algorithms:
see (Rémy, 2002, Sect. 2.4.2), for example. In that reference, and also in Pierce’s book (Pierce,
2002, Section 22.3), you will see an approach to type inference algorithms that views them as
part of the more general problem of generating and solving constraint problems. This seems
to be a fruitful viewpoint, because it accommodates a wide range of different type inference
problems.
3 POLYMORPHIC REFERENCE TYPES 25
3 Polymorphic Reference Types
3.1 The problem
Recall from the Introduction that an important purpose of type systems is to provide safety
via type soundness results (Slide 3). Even if a programming language is intended to be safe by
virtue of its type system, it can happen that separate features of the language, each desirable
in themselves, can combine in unexpected ways to produce an unsound type system. In this
section we look at an example of this which occurred in the development of the ML family of
languages. The two features which combine in a nasty way are:
• ML’s style of implicitly typed let-bound polymorphism, and
• reference types.
We have already treated the first topic in Section 2. The second concerns ML’s imperative fea-
tures, specifically its ability to dynamically create locally scoped storage locations which can
be written to and read from. We begin by giving the syntax and typing rules for this. We aug-
ment the grammar for Mini-ML types (Slide 13) with a unit type (a type with a single value)
and reference types; and correspondingly, we augment the grammar for Mini-ML expressions
(Slide 15) with a unit value, and operations for reference creation, dereferencing and assign-
ment. These additions are shown on Slide 32. We call the resulting language Midi-ML. The
typing rules for these new forms of expression are given on Slide 33.
ML types and expressions for mutable
references
t ::= . . .
| unit unit type
| t ref reference type
M ::= . . .
| () unit value
| ref M reference creation
| !M dereference
| M := M assignment
Slide 32
3 POLYMORPHIC REFERENCE TYPES 26
Midi-ML’s extra typing rules
(unit)
G ` () : unit
(ref)
G ` M : t
G ` ref M : t ref
(get)
G ` M : t ref
G ` !M : t
(set)
G ` M1 : t ref G ` M2 : t
G ` M1 := M2 : unit
Slide 33
Example
The expression
let r = ref lx (x) in
let u = (r := lx0 (ref !x0)) in
(!r)()
has type unit.
Slide 34
Example 5. Here is an example of the typing rules on Slide 33 in use. The expression given on
Slide 34 has type unit.
Proof. This can be deduced by applying the (let) rule (Slide 18) to the judgements
{ } ` ref lx (x) : (a � a) ref
r : 8a ((a � a) ref ) ` let u = (r := lx0 (ref !x0)) in (!r)() : unit.
The first of these judgements has the following proof:
3 POLYMORPHIC REFERENCE TYPES 27
(var �)
x : a ` x : a(fn)
{ } ` lx (x) : a � a
(ref)
{ } ` ref lx (x) : (a � a) ref
The second judgement can be proved by applying the (let) rule to
r : 8a ((a � a) ref ) ` r := lx0 (ref !x0) : unit (3)
r : 8a ((a � a) ref ), u : unit ` (!r)() : unit (4)
Writing G for the typing environment {r : 8a ((a � a) ref )}, the proof of (3) is
(var �)
G ` r : (a ref � a ref ) ref
(var �)
G, x0 : a ref ` x0 : a ref
(get)
G, x0 : a ref ` !x0 : a
(ref)
G, x0 : a ref ` ref !x0 : a ref
(fn)
G ` lx0 (ref !x0) : a ref � a ref
(set)
G ` r := lx0 (ref !x0) : unit
while the proof of (4) is
(var �)
G, u : unit ` r : (unit � unit) ref
(get)
G, u : unit ` !r : unit � unit
(var �)
G, u : unit ` () : unit
(app)
G, u : unit ` (!r)() : unit
Although the typing rules for references seem fairly innocuous, they combine with the
previous typing rules, and with the (let) rule in particular, to produce a type system for which
type soundness fails with respect to ML’s operational semantics. To see this we need to define
the operational semantics of Midi-ML.
Midi-ML transition system
Small-step transition relations
hM, si ! hM0, s0i
hM, si ! FAIL
where
I M, M0 range over Midi-ML expressions
I s, s0 range over states = finite functions
s = {x1 7! V1, . . . , xn 7! Vn} mapping variables xi to values Vi:
V ::= x | lx (M) | () | true | false | nil | V :: V
I configurations hM, si are required to satisfy that the free variables
of expression M are in the domain of definition of the state s
I symbol FAIL represents a run-time error
are inductively defined by syntax-directed rules. . .
Slide 35
3 POLYMORPHIC REFERENCE TYPES 28
The axioms and rules inductively defining the transition system for Midi-ML are those on Slide 36 together
with the following ones:
• hif true then M1 else M2, si ! hM1, si
• hif false then M1 else M2, si ! hM2, si
• hif V then M1 else M2, si ! FAIL, if V /2 {true, false}
• h(lx (M))V0, si ! hM[V0/x], si
• hV V0, si ! FAIL, if V not a function abstraction
• hlet x = V in M, si ! hM[V/x], si
• hcase nil of nil)M | x1 :: x2)M0, si ! hM, si
• hcase V1 :: V2 of nil)M | x1 :: x2)M0, si ! hM0[V1/x1, V2/x2], si
• hcase V of nil)M | x1 :: x2)M0, si ! FAIL, if V is neither nil nor a cons-value
•
hM, si ! hM0, s0i
hE [M], si ! hE [M0], s0i
•
hM, si ! FAIL
hE [M], si ! FAIL
where V ranges over values:
V ::= x | lx (M) | () | true | false | nil | V :: V
E ranges over evaluation contexts:
E ::= � | if E then M else M | E M | V E | let x = E in M | E :: M | V :: E
| case E of nil)M | x :: x)M | ref E | !E | E := M | V := E
and E [M] denotes the Midi-ML expression that results from replacing all occurrences of ‘�’ by M in E .
Figure 4: Transition system for Midi-ML
3 POLYMORPHIC REFERENCE TYPES 29
Midi-ML transitions involving references
h!x, si ! hs(x), si if x 2 dom(s)
h!V , si ! FAIL if V not a variable
hx := V 0, si ! h(), s[x 7! V 0]i
hV := V 0, si ! FAIL if V not a variable
href V , si ! hx, s[x 7! V ]i if x /2 dom(s)
where V ranges over values:
V ::= x | lx (M) | () | true | false | nil | V :: V
Slide 36
The operational semantics of Midi-ML uses an inductively defined transition relation of the
form shown on Slide 35 and which is inductively defined in Figure 4 and Slide 36 (using the
rather terse ‘evaluation contexts’ style of Wright and Felleisen (1994)). (The notation s[x 7! V]
used on Slide 36 means the state with domain of definition dom(s) [ {x} mapping x to V and
otherwise acting like s.)
*let r = ref lx (x) in
let u = (r := lx0 (ref !x0)) in (!r)() , {}
+
!⇤ hlet u = (r := lx0 (ref !x0)) in (!r)() , {r 7! lx (x)}i
!⇤ h(!r)() , {r 7! lx0 (ref !x0)}i
! hlx0 (ref !x0) () , {r 7! lx0 (ref !x0)}i
! href !() , {r 7! lx0 (ref !x0)}i
! FAIL
Slide 37
Returning to the expression on Slide 34, it evaluates as shown on Slide 37. Evaluation of
the outermost let-binding in M creates a fresh storage location bound to r and containing
3 POLYMORPHIC REFERENCE TYPES 30
the value lx (x). Evaluation of the second let-binding updates the contents of r to the value
lx0 (ref !x0) and binds the unit value to u. (Since the variable u does not occur in its body, M’s
innermost let-expression is just a way of expressing the sequence (r := lx0 (ref !x0)); (!r)()
in the fragment of ML that we are using for illustrative purposes.) Next (!r)() is evaluated.
This involves applying the current contents of r, which is lx0 (ref !x0), to the unit value ().
This results in an attempt to evaluate !(), i.e. to dereference something which is not a storage
location, an unsafe operation which should be trapped. Thus we have
hlet r = ref lx (x) in let u = (r := lx0 (ref !x0)) in (!r)(), { }i ! FAIL
3.2 Restoring type soundness
The root of the problem described in the previous section lies in the fact that typing expressions
like let r = ref M1 in M2 with the (let) rule allows the storage location (bound to) r to have a
type scheme s generalising the reference type of the type of M1. Occurrences of r in M2 refer to
the same, shared location and evaluation of M2 may cause assignments to this shared location
which restrict the possible type of subsequent occurrences of r. But the typing rule allows all
these occurrences of r to have any type which is a specialisation of s, and this can lead to unsafe
expressions being assigned types, as we have seen.
We can avoid this problem by devising a type system that prevents generalisation of type
variables occurring in the types of shared storage locations. A number of ways of doing this
have been proposed in the literature: see Wright (1995) for a survey of them. The one adopted
in the original, 1990, definition of Standard ML Milner et al. (1990) was that proposed by Tofte
(1990). It involves partitioning the set of type variables into two (countably infinite) halves, the
‘applicative type variables’ (ranged over by a) and the ‘imperative type variables’ (ranged over
by _a). The rule (ref) is restricted by insisting that t only involve imperative type variables;
in other words the principal type scheme of lx (ref x) becomes 8_a (_a � _a ref ), rather than
8a (a � a ref ). Furthermore, and crucially, the (let) rule (Slide 18) is restricted by requiring that
when the type scheme s = 8A (t) assigned to M1 is such that A contains imperative type
variables, then M1 must be a value (and hence in particular its evaluation does not create any
fresh storage locations).
This solution has the advantage that in the new system the typeability of expressions not
involving references is just the same as in the old system. However, it has the disadvantage that
the type system makes distinctions between expressions which are behaviourally equivalent
(i.e. which should be contextually equivalent). For example there are many list-processing
functions that can be defined in the pure functional fragment of ML by recursive definitions,
but which have more efficient definitions using local references. Unfortunately, if the type
scheme of the former is something like 8a (a list � a list), the type scheme of the latter may
well be the different type scheme 8_a (_a list � _a list). So we will not be able to use the two
versions of such a function interchangeably.
The authors of the revised, 1996, definition of Standard ML Milner et al. (1997) adopt a sim-
pler solution, proposed independently by Wright (1995). This removes the distinction between
applicative and imperative type variables (in effect, all type variables are imperative, but the
usual symbols a, a0 . . . are used) while retaining a value-restricted form of the (let) rule, as
shown on Slide 38.5 Thus our version of this type system is based upon exactly the same form
of type, type scheme and typing judgement as before, with the typing relation being generated
inductively by the axioms and rules on Slides 16–18 and 33, except that the applicability of the
(let) rule is restricted as on Slide 38.
5N.B. what we call a value, Milner et al. (1997) calls a non-expansive expression.
3 POLYMORPHIC REFERENCE TYPES 31
Value-restricted typing rule for let-expressions
(letv)
G ` M1 : t1 G, x : 8A (t1) ` M2 : t2
G ` let x = M1 in M2 : t2
(†)
(†) provided x /2 dom(G) and
A =
(
{ } if M1 is not a value
ftv(t1)� ftv(G) if M1 is a value
Recall that values are given by
V ::= x | lx (M) | () | true | false | nil | V :: V
Slide 38
Example 6. The expression on Slide 34 is not typeable in the type system for Midi-ML resulting
from replacing rule (let) by the value-restricted rule (letv) on Slide 38 (keeping all the other
axioms and rules the same).
Proof. Because of the form of the expression, the last rule used in any proof of its typeability
must end with (letv). Because of the side condition on that rule and since ref lx (x) is not a
value, the rule has to be applied with A = { }. This entails trying to type
let u = (r := lx0 (ref !x0)) in (!r)() (5)
in the typing environment G = {r : (a � a) ref}. But this is impossible, because the type variable
a is not universally quantified in this environment, whereas the two instances of r in (5) are of
different implicit types (namely (a ref � a ref ) ref and (unit � unit) ref ).
The above example is all very well, but how do we know that we have achieved safety with
this type system for Midi-ML? The answer lies in a formal proof of the type soundness property
stated on Slide 39. To prove this result, one first has to formulate a definition of typing for
general configurations hM, si when the state s is non-empty and then show
• typing is preserved under steps of transition,!;
• if a configuration can be typed, it cannot posses a transition to FAIL.
Thus a sequence of transitions from such a well-typed configuration can never lead to the FAIL
configuration. I do not give the details; the interested reader is referred to Wright and Felleisen
(1994); Harper (1994) for examples of similar type soundness results.
3 POLYMORPHIC REFERENCE TYPES 32
Type soundness for
Midi-ML with the value restriction
For any closed Midi-ML expression M, if there is some type
scheme s for which
` M : s
is provable in the value-restricted type system
(var �) + (bool) + (if) + (nil) + (cons) + (case) + (fn) +
(app) + (unit) + (ref) + (get) + (set) + (letv)
then evaluation of M does not fail,
i.e. there is no sequence of transitions of the form
hM,{ }i ! · · · ! FAIL
for the transition system ! defined in Figure 4
(where { } denotes the empty state).
Slide 39
In Midi-ML’s value-restricted type system, some expressions that
were typeable using (let) become untypeable using (letv).
For example (exercise):
let f = (lx (x)) ly (y) in ( f true) :: ( f nil)
But one can often1 use h-expansion
replace M by lx (M x) (where x /2 fv(M))
or b-reduction
replace (lx (M)) N by M[N/x]
to get around the problem.
(1 These transformations do not always preserve meaning [contextual
equivalence].)
Slide 40
Although the typing rule (letv) does allow one to achieve type soundness for polymor-
phic references in a pleasingly straightforward way, it does mean that some expressions not
involving references that are typeable in the original ML type system are no longer typeable
(Slide 40). Wright (1995, Sections 3.2 and 3.3) analyses the consequences of this and presents
evidence that it is not a hindrance to the use of Standard ML in practice.
4 POLYMORPHIC LAMBDA CALCULUS 33
4 Polymorphic Lambda Calculus
In this section we take a look at a type system for explicitly typed parametric polymorphism,
variously called the polymorphic lambda calculus (PLC), the second order typed lambda calculus, or
System F. It was invented by the logician Girard (1972) and, independently and for different
purposes, by the computer scientist Reynolds (1974). It has turned out to play a foundational
role in the development of type systems somewhat similar to that played by Church’s untyped
lambda calculus in the development of functional programming: although it is syntactically
very simple, it turns out that a wide range of types and type constructions can be represented
in the polymorphic lambda calculus.
l-bound variables in ML cannot be used
polymorphically within a function abstraction
For example, l f (( f true) :: ( f nil)) and l f ( f f ) are not
typeable in the Mini-ML type system.
Syntactically, because in rule
(fn)
G, x : t1 ` M : t2
G ` lx (M) : t1 � t2
the abstracted variable has to be assigned a trivial type scheme
(recall x : t1 stands for x : 8{ } (t1)).
Semantically, because 8A (t1)� t2 is not semantically
equivalent to an ML type when A 6= { }.
Slide 41
4.1 From type schemes to polymorphic types
We have seen examples (Example 2 and the first example on Slide 20) of the fact that the ML
type system permits let-bound variables to be used polymorphically within the body of a let-
expression. As Slide 41 points out, the same is not true of l-bound variables within the body
of a function abstraction. This is a consequence of the fact that ML types and type schemes
are separate syntactic categories and the function type constructor, �, operates on the former,
but not on the latter. Recall that an important purpose of type systems is to provide safety via
type soundness (Slide 3). Use of expressions such as those mentioned on Slide 41 does not seem
intrinsically unsafe (although use of the second one may cause non-termination—cf. the defi-
nition of the fixed point combinator in untyped lambda calculus). So it is not unreasonable to
seek type systems more powerful than the ML type system, in the sense that more expressions
become typeable.
One apparently attractive way of achieving this is just to merge types and type schemes
together: this results in the so-called polymorphic types shown on Slide 42. So let us consider
extending the ML type system to assign polymorphic types to expressions. So we consider
judgements of the form G ` M : p where:
• p is a polymorphic type;
4 POLYMORPHIC LAMBDA CALCULUS 34
• G = {x1 : p1, . . . , xn : pn} is a finite function from variables to polymorphic types.
In order to make full use of the mixing of � and 8 present in polymorphic types we have to
replace the axiom (var �) of Slide 16 by the rules shown on Slide 43. (These are in fact versions
for polymorphic types of valid properties of the original ML type system.) In rule (spec),
p[p0/a] indicates the polymorphic type resulting from substituting p0 for all free occurrences
of a in p.
Monomorphic types . . .
t ::= a | bool | t � t | t list
. . . and type schemes
s ::= t | 8a (s)
Polymorphic types
p ::= a | bool | p � p | p list | 8a (p)
E.g. a � a0 is a type, 8a (a � a0) is a type scheme and a polymorphic
type (but not a monomorphic type), 8a (a)� a0 is a polymorphic type,
but not a type scheme.
Slide 42
Identity, Generalisation and Specialisation
(id)
G ` x : p
if (x : p) 2 G
(gen)
G ` M : p
G ` M : 8a (p)
if a /2 ftv(G)
(spec)
G ` M : 8a (p)
G ` M : p[p0/a]
Slide 43
4 POLYMORPHIC LAMBDA CALCULUS 35
Example 7. In the modified ML type system (with polymorphic types and with (var �) re-
placed by (id), (gen), and (spec)) one can prove the following typings for expressions which
are untypeable in ML:
{ } ` l f (( f true) :: ( f nil)) : 8a (a � a)� bool list (6)
{ } ` l f ( f f ) : 8a (a)� 8a (a). (7)
Proof. The proof of (6) is rather easy to find and is left as an exercise. Here is a proof for (7):
(id)
f : 8a1 (a1) ` f : 8a1 (a1)(1)
f : 8a1 (a1) ` f : a2 � a2
(id)
f : 8a1 (a1) ` f : 8a1 (a1)(2)
f : 8a1 (a1) ` f : a2
(app)
f : 8a1 (a1) ` f f : a2
(gen)
f : 8a1 (a1) ` f f : 8a2 (a2)
(fn)
{ } ` l f ( f f ) : 8a1 (a1)� 8a2 (a2)
Nodes (1) and (2) are both instances of the (spec) rule: the first uses the substitution (a2 �
a2)/a1, whilst the second uses a2/a1.
ML + full polymorphic types
has undecidable type-checking
Fact (Wells, 1994). For the modified Mini-ML type system with
I full polymorphic types replacing types and type schemes
I (id) + (gen) + (spec) replacing (var �)
the type checking and typeability problems are undecidable.
Slide 44
So why does the ML programming language not use this extended type system with poly-
morphic types? The answer lies in the result stated on Slide 44: there is no algorithm to decide
typeability for this type system (Wells, 1994). The difficulty with automatic type inference for
this type system lies in the fact that the generalisation and specialisation rules are not syntax-
directed: since an application of either (gen) or (spec) does not change the expression M being
checked, it is hard to know when to try to apply them in the bottom-up construction of proof
inference trees. By contrast, in an ML type system based on (id), (gen) and (spec), but re-
taining the two-level stratification of types into monomorphic types and type schemes, this
difficulty can be overcome. For in that case one can in fact push uses of (spec) right up to the
leaves of a proof tree (where they merge with (id) axioms to become (var �) axioms) and push
uses of (gen) right down to the root of the tree (and leave them implicit, as we did on Slide 18).
4 POLYMORPHIC LAMBDA CALCULUS 36
The negative result on Slide 44 does not rule out the use of the polymorphic types of Slide 42
in programming languages, since one may consider explicitly typed languages (Slide 45) where
the tagging of expressions with type information renders the typeability problem essentially
trivial. A common view is that programming languages which enforce a large amount of ex-
plicit type information in programs are inconveniently verbose and/or force the programmer
to make algorithmically irrelevant decisions about typings. But of course it really depends
upon the intended applications. At one extreme, in a scripting language (interpreted inter-
actively, used by a single person to develop utilities in a rapid edit-run-debug cycle) implicit
typing may be desirable. Whereas at the opposite extreme, a language used to develop large
software systems (involving separate compilation of modules by different teams of program-
mers) may benefit greatly from explicit typing (not least as a form of documentation of pro-
grammer’s intentions, but also of course to enforce interfaces between separate program parts).
Apart from these issues, explicitly typed languages are useful as intermediate languages in opti-
mising compilers, since certain optimising transformations depend upon the type information
they contain. See Harper and Stone (1997), for example.
Explicitly versus implicitly typed languages
Implicit: little or no type information is included in program
phrases and typings have to be inferred, ideally, entirely at
compile-time. (E.g. Standard ML.)
Explicit: most, if not all, types for phrases are explicitly part of the
syntax. (E.g. Java.)
E.g. self application function of type 8a (a)� 8a (a)
(cf. Example 7)
Implicitly typed version: l f ( f f )
Explicitly type version: l f : 8a1 (a1) (La2 ( f (a2 � a2)( f a2)))
Slide 45
4 POLYMORPHIC LAMBDA CALCULUS 37
PLC syntax
Types
t ::= a type variable
| t � t function type
| 8a (t) 8-type
Expressions
M ::= x variable
| lx : t (M) function abstraction
| M M function application
| La (M) type generalisation
| M t type specialisation
(a and x range over fixed, countably infinite sets TyVar and Var
respectively.)
Slide 46
Functions on types
In PLC, La (M) is an anonymous notation for the function F
mapping each type t to the value of M[t/a] (of some particular
type).
F t denotes the result of applying such a function to a type.
Computation in PLC involves beta-reduction for such functions on
types
(La (M)) t ! M[t/a]
as well as the usual form of beta-reduction from l-calculus
(lx : t (M1)) M2 ! M1[M2/x]
Slide 47
4.2 The Polymorphic Lambda Calculus (PLC) type system
The explicit type information we need to add to expressions to get syntax-directed versions
of the (gen) and (spec) rules (Slide 43) concerns the operations of type generalisation and type
specialisation. These are forms of function abstraction and application respectively—for func-
tions defined on the collection of all types (and taking values in one particular type), rather
than on the values of one particular type. See Slide 47. The polymorphic lambda calculus,
4 POLYMORPHIC LAMBDA CALCULUS 38
PLC, provides rather sparse means for defining such functions—for example there is no type-
case construct that allows branching according to which type expression is input. As a result,
PLC is really a calculus of parametrically polymorphic functions (cf. Slide 8). The PLC syntax is
given on Slide 46. Its types, t, are like the polymorphic types, p, given on Slide 42, except
that we have omitted bool and (_) list—because in fact these and many other forms of datatype
are representable in PLC (see Section 4.4 below). We have also omitted let-expressions, be-
cause (unlike the ML type system presented in Section 2.1) they are definable from function
abstraction and application with the correct typing properties.
Remark 8 (Operator association and scoping). As in the ordinary lambda calculus, one often
writes a series of PLC applications without parentheses, using the convention that application
associates to the left. Thus M1 M2 M3 means (M1 M2)M3, and M1 M2 t3 means (M1 M2)t3.
Note that an expression like M1 t2 M3 can only associate as (M1 t2)M3, since association the
other way involves an ill-formed expression (t2M3). Similarly M1 t2 t3 can only be associated
as (M1 t2)t3 (since t1 t2 is an ill-formed type). On the other hand it is conventional to associate
a series of function types to the right. Thus t1 � t2 � t3 means t1 � (t2 � t3).
We delimit the scope of 8-, l-, and L-binders with parentheses. Another common way of
writing these binders employs ‘dot’ notation
8a .t lx : t . M La . M
with the convention that the scope extends as far to the right as possible. For example
8a1 . (8a2 . t � a1)� a1
means 8a1 (8a2 (t � a1) � a1). One often writes iterated binders using lists of bound (type)
variables:
8a1, a2 (t) , 8a1 (8a2 (t))
lx1 : t1, x2 : t2 (M) , lx1 : t1 (lx2 : t2 (M))
La1, a2 (M) , La1 (La2 (M)) .
It is also common to write a type specialisation by subscripting the type: Mt , M t.
Remark 9 (Free and bound (type) variables). Any occurrences in t of a type variable a become
bound in 8a (t). Thus by definition, the finite set, ftv(t), of free type variables of a type t, is given
by
ftv(a) , {a}
ftv(t1 � t2) , ftv(t1) [ ftv(t2)
ftv(8a (t)) , ftv(t)� {a}.
Any occurrences in M of a variable x become bound in lx : t (M). Thus by definition, the
finite set, fv(M), of free variables of an expression M, is given by
fv(x) , {x}
fv(lx : t (M)) , fv(M)� {x}
fv(M1 M2) , fv(M1) [ fv(M2)
fv(La (M)) , fv(M)
fv(M t) , fv(M).
4 POLYMORPHIC LAMBDA CALCULUS 39
Moreover, since types occur in expressions, we have to consider the free type variables of an
expression. The only type variable binding construct at the level of expressions is generalisation:
any occurrences in M of a type variable a become bound in La (M). Thus
ftv(x) , { }
ftv(lx : t (M)) , ftv(t) [ ftv(M)
ftv(M1 M2) , ftv(M1) [ ftv(M2)
ftv(La (M)) , ftv(M)� {a}
ftv(M t) , ftv(M) [ ftv(t).
As usual, we implicitly identify PLC types and expressions up to alpha-conversion of bound type vari-
ables and bound variables. For example
(lx : a (La (x a))) x and (lx0 : a (La0 (x0 a0))) x
are alpha-convertible. We will always choose names of bound variables as in the second ex-
pression rather than the first, i.e. distinct from any free variables (and from each other).
Remark 10 (Substitution). For PLC, there are three forms of (capture-avoiding) substitution,
well-defined up to alpha-conversion:
• t[t0/a] denotes the type resulting from substituting a type t0 for all free occurrences of
the type variable a in a type t.
• M[M0/x] denotes the expression resulting from substituting an expression M0 for all free
occurrences of the variable x in the expression M.
• M[t/a] denotes the expression resulting from substituting a type t for all free occur-
rences of the type variable a in an expression M.
The PLC type system uses typing judgements of the form shown on Slide 48. Its typing
relation is the collection of such judgements inductively defined by the axiom and rules on
Slide 49.
PLC typing judgement
takes the form G ` M : t where
I the typing environment G is a finite function from variables
to PLC types.
(We write G = {x1 : t1, . . . , xn : tn} to indicate that G has
domain of definition dom(G) = {x1, . . . , xn} and maps each
xi to the PLC type ti for i = 1 . . . n.)
I M is a PLC expression
I t is a PLC type.
Slide 48
4 POLYMORPHIC LAMBDA CALCULUS 40
PLC type system
(var)
G ` x : t
if (x : t) 2 G
(fn)
G, x : t1 ` M : t2
G ` lx : t1 (M) : t1 � t2
if x /2 dom(G)
(app)
G ` M : t1 � t2 G ` M0 : t1
G ` M M0 : t2
(gen)
G ` M : t
G ` La (M) : 8a (t)
if a /2 ftv(G)
(spec)
G ` M : 8a (t1)
G ` M t2 : t1[t2/a]
Slide 49
An incorrect proof
(var)
x1 : a, x2 : a ` x2 : a(fn)
x1 : a ` lx2 : a (x2) : a � a
(wrong!)
x1 : a ` La (lx2 : a (x2)) : 8a (a � a)
Slide 50
Remark 11 (Side-condition on rule (gen)). To illustrate the force of the side-condition on rule
(gen) on Slide 49, consider the last step of the incorrect proof on Slide 50. It is not a correct
instance of the (gen) rule, because the concluding judgement, whose typing environment G =
{x1 : a}, does not satisfy a /2 ftv(G) (since ftv(G) = {a} in this case). On the other hand, the
expression La (lx2 : a (x2)) does have type 8a (a � a) given the typing environment {x1 : a}.
Here is a correct proof of that fact:
4 POLYMORPHIC LAMBDA CALCULUS 41
(var)
x1 : a, x2 : a0 ` x2 : a0(fn)
x1 : a ` lx2 : a0 (x2) : a0 � a0
(gen)
x1 : a ` La0 (lx2 : a0 (x2)) : 8a0 (a0 � a0)
where we have used the freedom afforded by alpha-conversion to rename the bound type
variable to make it distinct from the free type variables of the typing environment: since we
identify types and expressions up to alpha-conversion, the judgement
x1 : a ` La (lx2 : a (x2)) : 8a (a � a)
is the same as
x1 : a ` La0 (lx2 : a0 (x2)) : 8a0 (a0 � a0)
and indeed, is the same as
x1 : a ` La0 (lx2 : a0 (x2)) : 8a00 (a00 � a00).
Example 12. On Slide 45 we claimed that l f : 8a1 (a1) (La2 ( f (a2 � a2)( f a2))) has type 8a (a)�
8a (a). Here is a proof of that in the PLC type system:
(var)
f : 8a1 (a1) ` f : 8a1 (a1)
(spec)
f : 8a1 (a1) ` f (a2 � a2) : a2 � a2
(var)
f : 8a1 (a1) ` f : 8a1 (a1)
(spec)
f : 8a1 (a1) ` f a2 : a2
(app)
f : 8a1 (a1) ` f (a2 � a2)( f a2) : a2
(gen)
f : 8a1 (a1) ` La2 ( f (a2 � a2)( f a2)) : 8a2 (a2)
(fn)
{ } ` l f : 8a1 (a1) (La2 ( f (a2 � a2)( f a2))) : (8a1 (a1))� 8a2 (a2)
Example 13. There is no PLC type t for which
{ } ` La ((lx : a (x)) a) : t (8)
is provable within the PLC type system.
Proof. Because of the syntax-directed nature of the axiom and rules of the PLC type system,
any proof of (8) would have to look like
(var)
x : a ` x : a(fn)
{ } ` lx : a (x) : t00
(spec)
{ } ` (lx : a (x)) a : t0
(gen)
{ } ` La ((lx : a (x)) a) : t
for some types t, t0 and t00. For the application of rule (fn) to be correct, it must be that
t00 = a � a. But then the application of rule (spec) is impossible, because a � a is not a 8-type.
So no such proof can exist.
4 POLYMORPHIC LAMBDA CALCULUS 42
Decidability of the PLC typeability and
type-checking problems
Theorem.
For each PLC typing problem, G ` M : ?, there is at most one
PLC type t for which G ` M : t is provable. Moreover there is an
algorithm, typ, which when given any G ` M : ? as input, returns
such a t if it exists and FAILs otherwise.
Corollary.
The PLC type checking problem is decidable: we can decide
whether or not G ` M : t is provable by checking whether
typ(G ` M : ?) = t.
(N.B. equality of PLC types up to alpha-conversion is decidable.)
Slide 51
4.3 PLC type inference
As Examples 12 and 13 suggest, the type checking and typeability problems (Slide 6) are very
easy to solve for the PLC type system, compared with the ML type system. This is because of
the explicit type information contained in PLC expressions together with the syntax-directed
nature of the typing rules. The situation is summarised on Slide 51. The uniqueness of types
property stated on the slide is easy to prove by induction on the structure of the expression M,
exploiting the syntax-directed nature of the axiom and rules of the PLC type system. Moreover,
the type inference algorithm typ emerges naturally from this proof, defined recursively accord-
ing to the structure of PLC expressions. The clauses of its definition are given on Slides 52
and 53.6 The definition relies upon the easily verified fact that equality of PLC types up to
alpha-conversion is decidable. It also assumes that the various implicit choices of names of
bound variables and bound type variables are made so as to keep them distinct from the rele-
vant free variables and free type variables. For example, in the clause for type generalisations
La (M), we assume the bound type variable a is chosen so that a /2 ftv(G).
6An implementation of this algorithm in Fresh OCaml can be found on the course web page.
4 POLYMORPHIC LAMBDA CALCULUS 43
PLC type-checking algorithm, I
Variables
typ(G, x : t ` x : ?) , t
Function abstractions
typ(G ` lx : t1 (M) : ?) ,
let t2 = typ(G, x : t1 ` M : ?) in t1 � t2
Function applications
typ(G ` M1 M2 : ?) ,
let t1 = typ(G ` M1 : ?) in
let t2 = typ(G ` M2 : ?) in
case t1 of t � t0 7! if t = t2 then t0 else FAIL
| _ 7! FAIL
Slide 52
PLC type-checking algorithm, II
Type generalisations
typ(G ` La (M) : ?) ,
let t = typ(G ` M : ?) in 8a (t)
Type specialisations
typ(G ` M t2 : ?) ,
let t = typ(G ` M : ?) in
case t of 8a (t1) 7! t1[t2/a]
| _ 7! FAIL
Slide 53
4.4 Datatypes in PLC
The aim of this subsection and the next is to give some impression of just how expressive is
the PLC type system. Many kinds of datatype, including both concrete data (booleans, natural
numbers, lists, various kinds of tree, . . . ) and also abstract datatypes involving information
hiding, can be represented in PLC. Such representations involve
• defining a suitable PLC type for the data,
4 POLYMORPHIC LAMBDA CALCULUS 44
• defining some PLC expressions for the various operations associated with the data,
• demonstrating that these expressions have both the correct typings and the expected
computational behaviour.
In order to deal with the last point, we first have to consider some operational semantics
for PLC. Most studies of the computational properties of polymorphic lambda calculus have
been based on the PLC analogue of the notion of beta-reduction from untyped lambda calculus.
This is defined on Slide 54.
Beta-reduction of PLC expressions
M beta-reduces to M0 in one step, M! M0 means M0 can
be obtained from M (up to alpha-conversion, of course) by
replacing a subexpression which is a redex by its corresponding
reduct.
The redex-reduct pairs are of two forms:
(lx : t (M1)) M2! M1[M2/x]
(La (M)) t! M[t/a]
M!⇤ M0 indicates a chain of finitely† many beta-reductions.
(† possibly zero – which just means M and M0 are alpha-convertible).
M is in beta-normal form if it contains no redexes.
Slide 54
Example 14. Here are some examples of beta-reductions. The various redexes are shown boxed.
Clearly, the final expression y is in beta-normal form.
(lx : a1 � a1 (x y)) (La2 (lz : a2 (z)))(a1 � a1)
yy ”
(La2 (lz : a2 (z)))(a1 � a1) y
&&
(lx : a1 � a1 (x y)) (lz : a1 � a1 (z))
ww
(lz : a1 � a1 (z))y
✏✏
y
4 POLYMORPHIC LAMBDA CALCULUS 45
Properties of PLC beta-reduction on typeable
expressions
Suppose G ` M : t is provable in the PLC type system. Then the
following properties hold:
Subject Reduction. If M! M0, then G ` M0 : t is also a
provable typing.
Church Rosser Property. If M!⇤ M1 and M!⇤ M2, then
there is M0 with M1!⇤ M0 and M2!⇤ M0.
Strong Normalisation Property. There is no infinite chain
M! M1! M2! . . . of beta-reductions starting from M.
Slide 55
PLC beta-conversion, =b
By definition, M =b M0 holds if there is a finite chain
M� ·� · · · � ·�M0
where each � is either! or , i.e. a beta-reduction in one
direction or the other. (A chain of length zero is allowed—in which
case M and M0 are equal, up to alpha-conversion, of course.)
Church Rosser + Strong Normalisation properties imply that, for
typeable PLC expressions, M =b M0 holds if and only if there is
some beta-normal form N with
M!⇤ N ⇤ M0
Slide 56
Slide 55 lists some important properties of typeable PLC expressions that we state without
proof. The first is a weak form of type soundness result (Slide 3) and its proof is straightfor-
ward. The proof of the Church Rosser property is also quite easy whereas the proof of Strong
Normalisations is difficult.7 It was first proved by Girard (1972) using a clever technique called
7Since it in fact implies the consistency of second order arithmetic, it furnishes a concrete example of Gödel’s
famous incompleteness theorem: the strong normalisation property of PLC is a statement that can be formalised
within second order arithmetic, is true (as witnessed by a proof that goes outside second order arithmetic), but
cannot be proved within that system.
4 POLYMORPHIC LAMBDA CALCULUS 46
‘reducibility candidates’; if you are interested in seeing the details, look at (Girard, 1989, Chap-
ter 14) for an accessible account of the proof.
Theorem 15. The properties listed on Slide 55 have the following consequences.
(i) Each typeable PLC expression, M, possesses a beta-normal form, i.e. an N such that M !⇤
N 9 , which is unique (up to alpha-conversion).
(ii) The equivalence relation of beta-conversion (Slide 56) between typeable PLC expressions is
decidable, i.e. there is an algorithm which, when given two typeable PLC expressions, decides
whether or not they are beta-convertible.
Proof. For (i), first note that such a beta-normal form exists because if we start reducing redexes
in M (in any order) the chain of reductions cannot be infinite (by Strong Normalisation) and
hence terminates in a beta-normal form. Uniqueness of the beta-normal form follows by the
Church Rosser property: if M!⇤ N1 and M!⇤ N2, then N1 !⇤ M0 ⇤ N2 holds for some M0;
so if N1 and N2 are beta-normal forms, then it must be that N1 !⇤ M0 and N2 !⇤ M0 are chains
of beta-reductions of zero length and hence N1 = M0 = N2 (equality up to alpha-conversion).
For (ii), we can use an algorithm which reduces the beta-redexes of each expression in any
order until beta-normal forms are reached (in finitely many steps, by Strong Normalisation);
these normal forms are equal (up to alpha-conversion) if and only if the original expressions
are beta-convertible. (And of course, the relation of alpha-convertibility is decidable.)
Remark 16. In fact, the Church Rosser property holds for all PLC expressions, whether or not
they are typeable. However, the Strong Normalisation property definitely fails for untypeable
expressions. For example, consider
W , (l f : a ( f f ))(l f : a ( f f ))
from which there is an infinite chain of beta-reductions, namely W ! W ! W ! · · · . As with
the untyped lambda calculus, one can regard polymorphic lambda calculus as a rather pure
kind of typed functional programming language in which computation consists of reducing
typeable expressions to beta-normal form. From this viewpoint, the properties on Slide 55 tell
us that (unlike the case of untyped lambda calculus) PLC cannot be ‘Turing powerful’, i.e. not
all partial recursive functions can be programmed in it (using a suitable encoding of numbers).
This is simply because, by virtue of Strong Normalisation, computation always terminates on
well-typed programs.
Now that we have explained PLC dynamics, we return to the question of representing
datatypes as PLC types. We consider first the simple example of booleans and then the more
complicated example of polymorphic lists.
4 POLYMORPHIC LAMBDA CALCULUS 47
Polymorphic booleans
bool , 8a (a � (a � a))
True , La (lx1 : a, x2 : a (x1))
False , La (lx1 : a, x2 : a (x2))
if , La (lb : bool, x1 : a, x2 : a (b a x1 x2))
Slide 57
Example 17 (Booleans). The PLC type corresponding to the ML datatype
datatype bool = True | False
is shown on Slide 57. The idea behind this representation is that the ‘algorithmic essence’ of a
boolean, b, is the operation lx1 : a, x2 : a (if b then x1 else x2) of type a � a � a,8 taking a
pair of expressions of the same type and returning one or other of them. Clearly, this operation
is parametrically polymorphic in the type a, so in PLC we can take the step of identifying
booleans with expressions of the corresponding 8-type, 8a (a � a � a). Note that for the PLC
expressions True and False defined on Slide 57 the typings
{ } ` True : 8a (a � a � a) and { } ` False : 8a (a � a � a)
are both provable. The if_then_else_ construct, given for the above ML datatype by a case-
expression
case M1 of True => M2 | False => M3
has an explicitly typed analogue in PLC, viz. if t M1 M2 M3, where t is supposed to be the
common type of M2 and M3 and if is the PLC expression given on Slide 57. It is not hard to
see that
{ } ` if : 8a (bool � (a � (a � a))).
Thus if G ` M1 : bool, G ` M2 : t and G ` M3 : t, then G ` if t M1 M2 M3 : t (cf. the typing rule
(if) on Slide 16). Furthermore, the expressions True, False, and if have the expected dynamic
behaviour:
• if M1 !⇤ True and M2 !⇤ N, then if t M1 M2 M3 !⇤ N;
• if M1 !⇤ False and M3 !⇤ N, then if t M1 M2 M3 !⇤ N.
It is in fact the case that True and False are the only closed beta-normal forms in PLC of type bool (up
to alpha-conversion, of course), but it is beyond the scope of this course to prove it.
8Recall our notational conventions: a � a � a means a � (a � a).
4 POLYMORPHIC LAMBDA CALCULUS 48
Iteratively defined functions on finite lists
A⇤ , finite lists of elements of the set A
Given a set B, an element x0 2 B, and a function f : A � B � B,
the iteratively defined function listIter x0 f is the unique
function g : A⇤ � B
satisfying:
g Nil = x0
g (x :: `) = f x (g `)
for all x 2 A and ` 2 A⇤.
Slide 58
Polymorphic lists
a list , 8a0 (a0 � (a � a0 � a0)� a0)
Nil , La, a0 (lx0 : a0, f : a � a0 � a0 (x0))
Cons , La(lx : a, ` : a list(La0(
lx0 : a0, f : a � a0 � a0(
f x (` a0 x0 f )))))
Slide 59
Example 18 (Lists). The polymorphic type corresponding to the ML datatype
datatype a list = Nil | Cons of a ⇤ (a list)
is shown on Slide 59. Undoubtedly it looks rather mysterious at first sight. The idea behind
this representation has to do with the operation of iteration over a list shown on Slide 58. The
existence of such functions listIter x0 f does in fact characterise the set A⇤ of finite lists over a
set A uniquely up to bijection. We can take the operation
lx0 : a0, f : a � a0 � a0 (listIter x0 f `) (9)
4 POLYMORPHIC LAMBDA CALCULUS 49
(of type a0� (a � a0� a0)� a0) as the ‘algorithmic essence’ of the list ` : a list. Clearly this oper-
ation is parametrically polymorphic in a0 and so we are led to the 8-type given on Slide 59 as
the polymorphic type of lists represented via the iterator operations they determine. Note that
from the perspective of this representation, the nil list is characterised as that list which when
any listIter x0 f is applied to it yields x0. This motivates the definition of the PLC expression Nil
on Slide 59. Similarly for the constructor Cons for adding an element to the head of a list. It is
not hard to prove the typings:
{ } ` Nil : 8a (a list)
{ } ` Cons : 8a (a � a list � a list).
As shown on Slide 60, an explicitly typed version of the operation of list iteration can be de-
fined in PLC: iter a a0 x0 f satisfies the defining equations for an iteratively defined function (9)
up to beta-conversion.
List iteration in PLC
iter , La, a0(lx0 : a0, f : a � a0 � a0(
l` : a list (` a0 x0 f )))
satisfies:
I ` iter : 8a, a0 (a0 � (a � a0 � a0)� a list � a0)
I iter a a0 x0 f (Nil a) =b x0
I iter a a0 x0 f (Cons a x `) =b f x (iter a a0 x0 f `)
Slide 60
Remark 19. The syntax of ML expressions we used in Section 2 featured the usual case-
expressions for lists. In PLC we might hope to define an expression case of type
8a, a00 (a00 � (a � a list � a00)� a list � a00)
such that
case a a00 x00 g (Nil a) = x00
case a a00 x00 g (Cons a x `) = g x `.
This is possible (but not too easy), by defining an operator for list primitive recursion. This
is alluded to on page 92 of Girard (1989); product types are mentioned there because the def-
inition of the primitive recursion operator can be done by a simultaneous iterative definition
of the operator itself and an auxiliary function. We omit the details. However, it is important
to note that the above equations will hold up to beta-conversion only for x and ` restricted to
range over beta-normal forms. (Alternatively, the equations hold in full generality so long as
‘=’ is taken to be some form of contextual equivalence.)
4 POLYMORPHIC LAMBDA CALCULUS 50
ML PLC
datatype null = ; null , 8a (a)
datatype unit = Unit; unit , 8a (a � a)
a1 ⇤ a2 a1 ⇤ a2 , 8a ((a1 � a2 � a)� a)
datatype (a1, a2)sum = (a1, a2)sum ,
Inl of a1 | Inr of a2; 8a ((a1 � a)� (a2 � a)� a)
datatype nat = nat ,
Zero | Succ of nat; 8a (a � (a � a)� a)
datatype binTree = binTree ,
Leaf | Node of binTree ⇤ binTree; 8a (a � (a � a � a)� a)
Figure 5: Some more algebraic datatypes
Booleans and lists are examples of ‘algebraic’ datatypes, i.e. ones which can be specified
(usually recursively) using products, sums and previously defined algebraic datatypes. Thus
in Standard ML such a datatype (called alg, with constructors C1, . . . , Cm) might be declared by
datatype (a1, . . . , an)alg = C1 of t1 | . . . | Cm of tm
where t1, . . . , tm are built up from the type variables a1, . . . , an and the type (a1, . . . , an)alg
itself, just using products and previously defined algebraic datatype constructors, but not,
for example, using function types. Figure 5 gives some other algebraic datatypes and their
representations as polymorphic types. In fact all algebraic datatypes can be represented in
PLC: see Girard (1989, Sections 11.3–5) for more details.
4.5 Existential types
Recall the notion of abstract data type, for example as provided by Standard ML’s notions of
signature and structure, illustrated on Slide 61. The signature QUEUE classifies structures con-
sisting of some type ’a queue and some values providing the usual operations on queues of
values of type ’a. The structure Queue matches this signature using a concrete representa-
tion of ’a queue (namely the type of pairs of ’a lists) which is hidden outside the structure
declaration. Mitchell and Plotkin (1988) observe that abstract data types can be classified by ex-
istentially quantified types; for example the signature QUEUE classifies structures for which there
exists a type ’a queue such that . . . .
4 POLYMORPHIC LAMBDA CALCULUS 51
Standard ML signatures and structures
signature QUEUE =
sig
type ’a queue
exception Empty
val empty : ’a queue
val insert : ’a * ’a queue -> ’a queue
val remove : ’a queue -> ’a * ’a queue
end
structure Queue =
struct
type ’a queue = ’a list * ’a list
exception Empty
val empty = (nil, nil)
fun insert (f, (front,back)) = (f::front, back)
fun remove (nil, nil) = raise Empty
| remove (front, nil) = remove (nil, rev front)
| remove (front, b::back) = (b, (front, back))
end
Slide 61
PLC + existential types
Types
t ::= · · · | 9 a (t)
Expressions
M ::= · · · | pack (t, M) : 9 a (t) |
unpack M : 9 a (t) as (a, x) in M : t
Typing rules
(9intro)
G ` M : t[t0/a]
G ` (pack (t0, M) : 9 a (t)) : 9 a (t)
(9elim)
G ` E : 9 a (t) G, x : t ` M0 : t0
G ` (unpack E : 9 a (t) as (a, x) in M0 : t0) : t0
if a /2 ftv(G, t0)
Reduction
unpack (pack (t0, M) : 9 a (t)) : 9 a (t)as (a, x)in M0 : t0 !
M0[t0/a, M/x]
Slide 62
Typing and reduction rules for an extension of PLC with existential types are given on
Slide 62. I have included rather a lot of explicit type information in the syntax of pack and
unpack expressions in order to keep type inference as simple as it is for pure PLC. Free oc-
currences of the type variable a in t become bound in the type 9 a (t); free occurrences of
the type variable a and the variable x in M0 become bound in the expression unpack E :
9 a (t) as (a, x) in M0 : t; and a should not occur free in the type t0 occurring at the end of an
unpack-expression – see the side condition on the typing rule (9elim), which is comparable to
the side condition on the PLC typing rule (gen).
4 POLYMORPHIC LAMBDA CALCULUS 52
Existential types in PLC
9 a (t) , 8b ((8a (t � b))� b)
pack (t0, M) : 9 a (t) , Lb (ly : 8a (t � b) (y t0M))
unpack E : 9 a (t) as (a, x) in M0 : t0 , E t0(La (lx : t (M0)))
(where b /2 ftv(a t t0 M M0))
These definitions satisfy the typing and reduction rules on the
previous slide (exercise).
Slide 63
In fact this extension of PLC with existential types does not increase its expressive power,
because it is possible to translate the extended type system back into pure PLC, as indicated
on Slide 63.
5 DEPENDENT TYPES 53
5 Dependent Types
In the Mini-ML language, expressions (Slide 15) can depend upon variables, in the sense that
they can contain occurrences of free variables; and Mini-ML type schemes can depend upon
type variables. In PLC (Slide 46), expressions can depend upon both variables and type vari-
ables, but types can only depend upon type variables. Is it useful to consider type systems
in which the types depend upon variables (and possibly upon type variables as well)? The
answer is an emphatic yes. Such dependently-typed systems go back to the pioneering work of
the logician Martin-Löf (1975) and mathematician de Bruijn (1970), and are still the subject of
vigorous research by people interested in functional programming languages and in machine-
checked formalisation of mathematics. The next subsection gives a small example to illustrate
why it is useful to consider types that depend on variables ranging over the values of another
type.
5.1 Dependent functions
It is helpful to recall some discrete mathematics. If A and B are sets, then the set A � B of
mathematical functions from A to B is by definition the set of binary relations F ✓ A⇥ B that
are single-valued
8a 2 A, b 2 B, b0 2 B ((a, b) 2 F ^ (a, b0) 2 F � b = b0)
and total
8a 2 A (9b 2 B ((a, b) 2 F)).
Suppose now instead of a single set B we are given a family of sets Ba indexed by elements
a 2 A. (In other words {(a, Ba) | a 2 A} is a mathematical function from A into a set of sets.)
Defining
B ,
S
a2A Ba = {b | 9a 2 A (b 2 Ba)}
to be the union of the sets Ba as a ranges over all the elements of A, we can consider those
mathematical functions F 2 A � B with the property that F maps each a 2 A into the set Ba;
see Slide 64.
Dependent Functions
Given a set A and a family of sets Ba indexed by the elements a of
A, we get a set
’a2A Ba , {F 2 A �
S
a2A Ba | 8(a, b) 2 F (b 2 Ba)}
of dependent functions. Each F 2 ’a2A Ba is a single-valued
and total relation that associates to each a 2 A an element in Ba
(usually written F a).
For example if A = N and for each n 2 N, Bn = {0, 1}n � {0, 1}, then
’n2N Bn consists of functions mapping each number n to an n-ary
Boolean operation.
5 DEPENDENT TYPES 54
Slide 64
A tautology checker
fun taut x f = if x = 0 then f else
(taut(x � 1)( f true))
andalso (taut(x � 1)( f false))
Defining types n AryBoolOp for each natural number n 2 N
(
0 AryBoolOp , bool
(n + 1)AryBoolOp , bool � (n AryBoolOp)
then taut n has type (n AryBoolOp)� bool, i.e. the result type
of the function taut depends upon the value of its argument.
Slide 65
Now consider programming, in Standard ML say, a function taut that for any number n
takes in n-ary boolean operations (in ‘curried’ form)
f : bool � bool � · · · bool�| {z }
n arguments
bool
and returns true if f is a tautology. In other words taut f has value true if f gives true when
applied to all of its 2n possible arguments, and otherwise taut f has value false. One might try to
program taut in Standard ML as on Slide 65. This is algorithmically correct, but does not type-
check in ML. Why? Intuitively, the type of taut n for each natural number n = 0, 1, 2, . . . is the
type n AryBoolOp of ‘n-ary curried boolean operations’ defined (by induction on n) on Slide 65.
Then taut really should be a dependently typed function—the type of its result depends on
the value of the argument supplied to it—and so it is rejected by the ML type-checker, because
ML does not permit such dependence in its types. Slide 66 programs the tautology-checker in
Agda (wiki.portal.chalmers.se/agda/agda.php), a popular dependently typed functional
programming language with syntax reminiscent of Haskell (www.haskell.org).
In general a dependent type is a type expression containing a free variable for which expres-
sions ranging over some type can be substituted For example, on Slide 66 the type expression
x AryBoolOp contains a variable x for which we can substitute expressions e of Type Nat to get
types e AryBoolOp (which are themselves expressions of the Agda type Set).
5 DEPENDENT TYPES 55
The tautology checker in Agda
data Bool : Set where
true : Bool
false : Bool
_and_ : Bool -> Bool -> Bool
true and true = true
true and false = false
false and _ = false
data Nat : Set where
zero : Nat
succ : Nat -> Nat
_AryBoolOp : Nat -> Set
zero AryBoolOp = Bool
(succ x) AryBoolOp = Bool -> x AryBoolOp
taut : (x : Nat) -> x AryBoolOp -> Bool
taut zero f = f
taut (succ x) f = taut x (f true) and taut x (f false)
Slide 66
Some typing rules for dependent function types are given on Slide 67, using the (more
common) notation Px : t (t0) for what Agda writes as (x : t) � t0. Compare them with the
usual rules for non-dependent function types t � t0 (Slide 18); note that those rules are the
special case of the ones on Slide 67 where the type t0 has no free occurrences of the variable x.
Dependent function types Px : t (t0)
G, x : t ` M : t0
G ` lx : t (M) : Px : t (t0)
if x /2 dom(G)
G ` M : Px : t (t0) G ` M0 : t
G ` M M0 : t0[M0/x]
t0 may ‘depend’ on x, i.e. have free occurrences of x.
(Free occurrences of x in t0 are bound in Px : t (t0).)
Slide 67
5 DEPENDENT TYPES 56
Conversion typing rule
Dependent type systems usually feature a rule of the form
G ` M : t
G ` M : t0
if t ⇡ t0
where t ⇡ t0 is some relation of equality between types
(e.g. inductively defined in some way).
For example one would expect (1 + 1) AryBoolOp ⇡ 2 AryBoolOp.
For decidability of type-checking, one needs ⇡ to be a decidable
relation between type expressions.
Slide 68
For reasons that we will explore in Section 6, type theories with dependent types have
been used extensively in computer systems for formalising mathematics, for proof construc-
tion, and for checking the correctness of proofs. In this respect Martin-Löf’s intuitionistic type
theory (which first popularised the notion of ‘dependent type’) has been highly influential; see
Nordström et al. (1990) for an introduction. The Agda language is based upon it (and as it
says on its home page, ‘Agda is a proof assistant’ as well as a dependently typed functional
programming language). A related and increasingly popular example of such a system is
Coq (coq.inria.fr), which is based on a dependent type theory called the Calculus of Induc-
tive Constructions.
Type systems featuring dependent types are able to express much more refined proper-
ties of programs than ones without this feature. So why do they not get used routinely in
general-purpose programming languages? The answer lies in the fact that type-checking with
dependent types naturally involves checking equalities between the data values upon which
the types depend: see Slide 68. For example, if we add to the Agda code in Slide 66 a definition
of the addition function
_plus_ : Nat -> Nat -> Nat
n plus Zero = n
n plus (Succ n’) = Succ(n plus n’)
then terms of type
((Succ Zero)plus(Succ Zero))AryBoolOp
should also be terms of type
(Succ(Succ(Zero)))AryBoolOp
In a ‘Turing-powerful’ language, that is one whose programs can express all computable par-
tial functions9, one would expect such value-equality to be undecidable and hence static type-
checking becomes impossible. How to get round this problem is an active area of research.
9Agda is not by default Turing powerful, because by design only total functions are programmable in it –
reflecting its intended use as a proof assistant.
5 DEPENDENT TYPES 57
For example the Cayenne language (Augustsson, 1998) takes a general-purpose, pragmatic,
but incomplete approach; whereas Xi and Pfenning (1998) uses dependent types for a specific
task, namely static elimination of run-time array bound checking, by restricting dependency
to a language of integer expressions where checking equality reduces to solving linear pro-
gramming problems. Haskell (and later versions of OCaml) incorporate many ideas from de-
pendently typed systems while maintaining static type-checking. For further reading on type
systems with dependent-types I recommend Aspinall and Hofmann (2005).
5.2 Pure Type Systems
Pure Type Systems (Barendregt, 1992, Sect. 5.2) is a family of dependently-typed languages for
expressing various kinds of polymorphic function abstraction. PLC is in this family and the
general case of a Pure Type System is syntactically as simple as PLC. However, the family of
Pure Type Systems contains other instances that go well beyond PLC in the kind of function
abstraction they can express. Two examples are Girard’s System F-omega, which Greg Morrisett
in some lectures from 2005 calls “the workhorse of modern compilers” and the Calculus of
Constructions of Coquand and Huet (1988), which forms an important part of the logical basis of
the popular Coq proof assistant (coq.inria.fr). Barendregt analysed the forms of abstraction
present in the Calculus of Constructions by introducing a cube of related typed l-calculi; and
Pure Type Systems were introduced by Berardi and Terlouw as a natural generalisation of
Barendregt’s l-cube.
Pure Type Systems (PTS) – syntax
In a PTS type expressions and term expressions are lumped
together into a single syntactic category of pseudo-terms:
t ::= x variable
| s sort
| Px : t (t) dependent function type
| lx : t (t) function abstraction
| t t function application
where x ranges over a countably infinite set Var of variables and s ranges over
a disjoint set Sort of sort symbols – constants that denote various universes
(= types whose elements denote types of various sorts) [kind is a commonly
used synonym for sort]. lx : t (t0) and Px : t (t0) both bind free occurrences
of x in the pseudo-term t0.
t[t0/x] denotes result of capture-avoiding substitution of t0 for all
free occurrences of x in t.
t � t0 , Px : t (t0) where x /2 fv(t0).
Slide 69
The syntax of Pure Type Systems (PTS) is given on Slide 69. There is a single collection
of pseudo-terms, some of which denote types and some of which denote elements of types.
Operator association, scoping, free and bound variables and substitution are like those for the
l-calculus and PLC:
Remark 20 (Operator association and scoping). As usual, application associates to the left. We
continue to delimit the scope of P- and l-binders with parentheses, but ‘dot’ notation is also
5 DEPENDENT TYPES 58
very common in the literature
Px : t. t0 lx : t. t0
in which case the scope of the binder extends as far to the right of the dot as possible. For
iterated bindings we will surpress the repeated P or l symbols and write just one followed by
a list of typed variables.
Remark 21 (Free and bound variables; substitution). Any free occurrences of x in a pseudo-
term t0 become bound in lx : t (t0) and Px : t (t0). Thus the finite set fv(t) of free variables of a
pseudo-term t is given by:
fv(x) = {x}
fv(s) = { }
fv(Px : t (t0)) = fv(t) [ (fv(t0)� {x})
fv(lx : t (t0)) = fv(t) [ (fv(t0)� {x})
fv(t t0) = fv(t) [ fv(t0)
As usual, we implicitly identify pseudo-terms up to alpha-conversion of bound variables. t[t0/x] de-
notes the capture-avoiding substitution of t0 for all free occurrences of x in the pseudo-term
t.
Pure Type Systems – beta-conversion
I beta-reduction of pseudo-terms: t ! t0 means t0 can be
obtained from t (up to alpha-conversion, of course) by
replacing a subexpression which is a redex by its
corresponding reduct. There is only one form of redex-reduct
pair:
(lx : t (t1)) t2 ! t1[t2/x]
I As usual, !⇤ denotes the reflexive-transitive closure of !.
I beta-conversion of pseudo-terms: =b is the
reflexive-symmetric-transitive closure of ! (i.e. the smallest
equivalence relation containing !).
Slide 70
As remarked on Slide 68 for dependently-typed systems in general, typing in PTS involves
a notion of equality between pseuodo-expressions: PTS uses the usual notion of beta-conversion
from the l-calculus (Slide 70). The form of PTS typing judgements is shown on Slide 72 and
the rues for generating the derivable judgements on Slide 73; the notation dom(G) used there
refers to the domain of a context G:
dom(⇧) = { }
dom(G, x : t) = dom(G) [ {x}.
The rules on Slide 73 are parameterized by a specification, defined on slide 71. We write lS for
the PTS with specification S.
5 DEPENDENT TYPES 59
Pure Type Systems – specifications
The typing rules for a particular PTS are parameterised by a
specification S = (S ,A,R) where:
I S ✓ Sort
Elements s 2 S denote the di�erent universes of types in this PTS.
I A ✓ Sort ⇥ Sort
Elements (s1, s2) 2 A are called axioms. They determine the
typing relation between universes in this PTS.
I R ✓ Sort ⇥ Sort ⇥ Sort
Elements (s1, s2, s3) 2 R are called rules. They determine which
kinds of dependent function can be formed and in which universes
they live.
The PTS with specification S will be denoted lS .
Slide 71
Pure Type Systems – typing judgements
take the form
G ` t : t0
where t, t0 are pseudo-terms and G is a context, a form of typing
environment given by the grammar
G ::= ⇧ | G, x : t
(Thus contexts are finite ordered lists of (variable,pseudo-term)-pairs,
with the empty list denoted ⇧, the head of the list on the right and
list-cons denoted by _, _. Unlike previous type systems in this course,
the order in which typing declarations x : t occur in a context is
important.)
A typing judgement is derivable if it is in the set inductively
generated by the rules on the next slide, which are parameterised
by a given specification S = (S ,A,R).
Slide 72
5 DEPENDENT TYPES 60
Pure Type Systems – typing rules
(axiom)
⇧ ` s1 : s2
if (s1, s2) 2 A
(start)
G ` A : s
G, x : A ` x : A
if x /2 dom(G)
(weaken)
G ` M : A G ` B : s
G, x : B ` M : A
if x /2 dom(G)
(conv)
G ` M : A G ` B : s
G ` M : B
if A =b B
(prod)
G ` A : s1 G, x : A ` B : s2
G ` Px : A (B) : s3
if (s1, s2, s3) 2 R
(abs)
G, x : A ` M : B G ` Px : A (B) : s
G ` lx : A (M) : Px : A (B)
(app)
G ` M : Px : A (B) G ` N : A
G ` M N : B[N/x]
(A, B, M, N range over pseudoterms, s, s1, s2, s3 over sort symbols)
Slide 73
Example PTS typing derivations
(axiom) ⇧ ` ⇤ : ⇤
(axiom) ⇧ ` ⇤ : ⇤ (axiom) ⇧ ` ⇤ : ⇤(weaken) ⇧, x : ⇤ ` ⇤ : ⇤
(prod) ⇧ ` ⇤� ⇤ : ⇤
(axiom) ⇧ ` ⇤ : ⇤(start) ⇧, x : ⇤ ` x : ⇤
…
⇧ ` ⇤� ⇤ : ⇤
(abs)
⇧ ` lx : ⇤ (x) : ⇤� ⇤
Here we assume that the PTS specification S = (S ,A,R) has ⇤ 2 S ,
⇤ 2 S , (⇤,⇤) 2 A and (⇤,⇤,⇤) 2 R.
(Recall that ⇤� ⇤ , Px : ⇤ (⇤).)
Slide 74
Slide 74 illustrates how PTS typing derivations begin, using (axiom), (start) and (weaken).
Note that the rules (conv) and (prod) feature extra hypotheses (compared with what one
might expect, for example from Slide 68) which ensure that every pseudo-term that appears
in a position in a derivable judgement where a type is expected has a sort, or is already a sort.
This is the Correctness of types property on Slide 75. Note that the rules on Slide 73 are not all
syntax-directed; in particular, in a syntax-directed search for a type for a given pseudo-term, it
is not clear when rule (conv) should be used. For this reason the type-checking and typeability
problems (Slide 6) for a PTS can be difficult: for some PTS specifications these problems are
5 DEPENDENT TYPES 61
decidable (and good algorithms are known – see Barthe (1999) for example), and for some they
are not. Slide 76 states two results of this kind.
Properties of Pure Type Systems in general
I Correctness of types. If G ` M : A, then either A 2 S , or
G ` A : s for some s 2 S .
I Church-Rosser Property (aka confluence). t =b t0 i�
9u (t !⇤ u ^ t0 !⇤ u)
I Subject Reduction. If G ` M : A and M ! M0, then
G ` M0 : A.
I Uniqueness of Types. A PTS specification S = (S ,A,R)
is said to be functional if both A and
Rs , {(s2, s3) | (s, s2, s3) 2 R} for each s 2 S , are
single-valued binary relations.
In this case lS satisfies: if G ` M : A and G ` M : B, then
A =b B.
Slide 75
Type-checking for a PTS, lS
Definition. A pseudo-term t is legal for a PTS specification
S = (S ,A,R) if either t 2 S or G ` t : t0 is derivable in lS for
some G and t0.
Recall the type-checking and typeability problems for a type
system.
Fact(van Bentham Jutting): these problems for lS are decidable
if S is finite and lS is normalizing, meaning that for every legal
pseudo-term there is some finite chain of beta-reductions leading
to a beta-normal form.
Fact (Meyer): the problems are undecidable for the PTS l⇤ with
specification S = {⇤}, A = {(⇤,⇤)} and R = {(⇤,⇤,⇤)}.
Slide 76
Remark 22 (Equality judgements). Pure Type Systems are a good first example of formally
defined type systems featuring dependent types, because they are syntactically quite simple.
In particular, they have only one form of judgement (Slide 72) and a notion of equality (=b)
which is defined independently of typing. In contrast, many type systems for dependent types
5 DEPENDENT TYPES 62
feature both a typing judgement G ` M : A and an equality judgement
G ` M ⌘ M0 : A
defined mutually inductively. For example, if one wanted equality to satisfy h-conversion, it
makes sense to equate M with lx : A (M x) only if M is already known to have a (dependent)
function type:
G ` M : Px : A (B)
if x /2 fv(M)
G ` M ⌘ lx : A (M x) : Px : A (B)
For example, see the type system lLF in the chapter by Aspinall and Hofmann (2005).
In the rest of this section and the next we give some examples of Pure Type Systems.
Example 23 (PLC as a Pure Type System). Consider the PTS signature on Slide 77. The sort
⇤ plays a trivial, but important role: the only pseudo-term t satisfying ⇧ ` t : ⇤ is t = ⇤.
The sort ⇤ classifies types in l2. Because we have ⇧ ` ⇤ : ⇤ we can use the rules (start) and
(weaken) to introduce type variable G, a : ⇤ ` a : ⇤ (assuming a 2 Var). Then the typing
rule (prod) for rule (⇤, ⇤, ⇤) 2 R2 allows the formation of types G ` Pa : ⇤ (t) : ⇤, given
that G, a : ⇤ ` t : ⇤ is derivable – these behave like PLC’s 8a (t) types. The other rule in
the specification, (⇤, ⇤, ⇤) 2 R2, allows the formation of types G ` Px : t (t0) : ⇤, given that
G ` t : ⇤ and G, x : t ` t0 : ⇤ is derivable. In fact legal pseudo-terms in l2 of type ⇤ can
only involve free type variables, but not free variables of some given type t : ⇤; so the l2 type
Px : t (t0) is in fact the simple function type t � t0, rather than a properly dependent function
type.
As the above remarks suggest, there is a strong relationship between l2 and the Polymor-
phic Lambda Calculus (Section 4). For example the polymorphic identity function in PLC
{ } ` La (lx : a (x)) ` 8a (a � a)
corresponds in the PTS l2 to
⇧ ` la : ⇤ (lx : a (x)) : Pa : ⇤ (a � a) (10)
(I am making the simplifying assumption that the set of variables from which l2 pseudo-terms
are formed consists of the disjoint union of the sets of type variables and variables used in PLC
type and term expressions.)
In fact the PTS l2 and PLC are essentially the same type system. Using the translation
of PLC types and terms into l2 pseudo-terms given on Slide 77 one can show the properties
on Slide 78. The proof of these properties necessarily involves considering PLC typing judge-
ments with non-empty typing environments and the mis-match between how I defined those
and how PTS contexts are defined makes statements and proofs messy: it would be better to
reformulate PLC using typing environments that are lists (rather than finite functions) and that
record the use of free type variables in the environment (rather than leaving that information
implicit as I did in Section 4).
5 DEPENDENT TYPES 63
PLC versus the Pure Type System l2
PTS signature:
2 , (S2,A2,R2) where
8
<
:
S2 , {⇤,⇤}
A2 , {(⇤,⇤)}
R2 , {(⇤,⇤,⇤), (⇤,⇤,⇤)}
Translation of PLC types and terms to l2 pseudo-terms:
JaK = a
Jt � t0K = Px : JtK (Jt0K)
J8a (t)K = Pa : ⇤ (Jt0K)
JxK = x
Jlx : t (M)K = lx : JtK (JMK)
JM M0K = JMK JM0K
JLa (M)K = la : ⇤ (JMK)
JM tK = JMK JtK
Slide 77
Properties of the translation from PLC to l2
I If { } ` M : t is derivable in PLC, then ⇧ ` JtK : ⇤ and
⇧ ` JMK : JtK are derivable in l2
I In l2, if ⇧ ` t : ⇤, then t = ⇤; if ⇧ ` t : ⇤, then t = JtK for
some closed PLC type t; and if ⇧ ` t : t0 then t = JMK and
t0 = JtK for PLC expressions satisfying { } ` M : t.
I Under the translation, the reduction behaviour of PLC terms
is preserved and reflected by beta-reduction in l2. (Note in
particular that PLC types are translated to pseudo-terms in
beta-normal form.)
Slide 78
5.3 System Fw
I mentioned at the start of Section 4 that PLC was invented by the logician Jean-Yves Girard,
under the name System F, as part of his seminal work on the proof-theory of second-order
arithmetic. In fact, as the name suggests (Interprétation fonctionelle et élimination des coupures
dans l’arithmetique d’ordre supérieur), the work of Girard (1972) treats the proof theory of not
just second-order, but also higher-order arithmetic. (I discuss what Type Systems have to do
with proofs and their theory in Section 6.) To do so he introduced a higher-order version
5 DEPENDENT TYPES 64
of Polymorphic Lambda Calculus, called System Fw. From a programming language (rather
than a logic) point of view, System Fw allows us to write functions that are parametrically
polymorphic not only in types, but also in type constructions (functions from types to types)
and higher-order versions of such constructions. Fw can be defined as an instance of the notion
of Pure Type System: see Slide 79.
System Fw as a Pure Type System: lw
PTS specification w = (Sw,Aw,Rw):
Sw , {⇤,⇤}
A , {(⇤,⇤)}
R , {(⇤,⇤,⇤), (⇤,⇤,⇤), (⇤,⇤,⇤)}
As in l2, sort ⇤ is a universe of types; but in lw, the rule (prod) for
(⇤,⇤,⇤) means that ⇧ ` t : ⇤ holds for all the ‘simple types’ over the
ground type ⇤ – the ts generated by the grammar t ::= ⇤ | t � t
Hence rule (prod) for (⇤,⇤,⇤) now gives many more legal pseudo-terms
of type ⇤ in lw compared with l2 (PLC), such as
⇧ ` (PT : ⇤� ⇤ (Pa : ⇤ (a � T a))) : ⇤
⇧ ` (PT : ⇤� ⇤ (Pa, b : ⇤ ((a � T b)� T a � T b))) : ⇤
Slide 79
Fw underlies work on type-directed compilation of strongly-typed functional program-
ming languages to lower-level languages (Greg Morrisett in some lectures from 2005 calls Fw
the “the workhorse of modern compilers”). Later versions of Haskell and OCaml give the
programmer access to such higher-order polymorphism.
As an example of the kind of type abstractions that Fw provides, consider the concept of a
monad from the mathematical theory of categories (MacLane, 1971, Chapter VI), widely used
in typed functional programming to tame ‘impure’ forms of computation, such as exceptions,
I/O, or foreign language calls; see Wadler (1992) and Peyton Jones (2001). In Standard ML,
a monad is specified by the data on Slide 80: one thinks of values of type t(a) as denoting
computations of some kind that produce values of type a. For example in the global state
monad, a computation in s � (a ⇤ s) takes in an initial state represented as a value of type
s and returns, if anything, a pair consisting of a value of type a and a final state. Not only
are there many different monads, but also there are lots of useful ways of transforming and
combining existing monads to form new ones. To express such monad transformers we need a
way of abstracting over the data specifying a monad – in particular of writing functions with
arguments T : ⇤� ⇤, where ⇤ is a sort of types. Fw allows us to do this; see Slide 81.
5 DEPENDENT TYPES 65
Monads in ML
A monad in ML is given by type t(a) with a free type variable a
together with expressions
unit : a � t(a)
lift : (a � t(b))� t(a)� t(b)
(writing t(b) for the result of replacing a by b in t) satisfying
some equational properties [omitted].
E.g.
I list monad t(a) = a list
I global state monad t(a) = s � (a ⇤ s) (for some type s of states)
I simple exception monad t(a) = (a, #)sum (for some type # of
exception names)
[definitions of unit and lift in each case omitted]
Slide 80
Examples of lw type constructions
I Product types (cf. the PLC representation of product types):
P , la, b : ⇤ (Pg : ⇤ ((a � b � g)� g))
⇧ ` P : ⇤� ⇤� ⇤
I Monad transformer for state (using a type ⇧ ` S : ⇤ for
states):
M , lT : ⇤� ⇤ (la : ⇤ (S � T(P a S)))
⇧ ` M : (⇤� ⇤)� ⇤� ⇤
I Existential types (cf. the PLC representation of existential
types):
9 , lT : ⇤� ⇤ (Pb : ⇤ ((Pa : ⇤ (T a � b))� b))
⇧ ` 9 : (⇤� ⇤)� ⇤
Slide 81
5 DEPENDENT TYPES 66
Type-checking for Fw
Fact (Girard): System Fw is strongly normalizing in the sense
that for any legal pseudo-term t, there is no infinite chain of
beta-reductions t ! t1 ! t2 ! · · · .
As as corollary we have that the type-checking and typeability
problems for Fw are decidable.
Slide 82
One of the important results of Girard (1972) is that Systems F and Fw are strongly normaliz-
ing; see Slide 82. His proof introduced the ‘candidates of reducibility’ method, which has been
successfully generalized to other dependently-typed lambda calculi. Girard (1989, Chapter 14)
gives the method applied to PLC.
6 PROPOSITIONS AS TYPES 67
6 Propositions as Types
The concept of ‘type’ first arose in the logical foundations of mathematics. Russell (1903) cir-
cumvented the paradox he discovered in Frege’s set theory by stratifying the universe of un-
typed sets into levels, or types. Church (1940) proposed a typed, higher order logic based
on functions rather than sets and which is capable of formalising large areas of mathematics.
A version of this logic is the one underlying the HOL system (Gordon and Melham, 1993).
See Lamport and Paulson (1999) for a stimulating discussion of the pros and cons of untyped
logics (typically, set theory) versus typed logics for mechanising mathematics. The interplay
between logic and types has often been mediated by the correspondence between proofs in
certain systems of logic and the terms in certain typed lambda calculi. This was first noted by
the logician Curry in the 1950s and brought to the attention of computer scientists by the work
of Howard in the 1980s. As a result, this connection between logic and type systems is often
known as the Curry-Howard correspondence. If is also known as propositions-as-types for reasons
that I explain in Sect. 6.2. Before that, I make an digression into intuitionistic, or constructive
logic, since it is that kind of logic for which the Curry-Howard correspondence first arose.
Constructive interpretation of logic
I Implication: a proof of j� y is a construction that
transforms proofs of j into proofs of y.
I Negation: a proof of ¬j is a construction that from any
(hypothetical) proof of j produces a contradiction (= proof of
falsity ?)
I Disjunction: a proof of j_ y is an object that manifestly is
either a proof of j, or a proof of y.
I For all: a proof of 8x (j(x)) is a construction that
transforms the objects a over which x ranges into proofs of
j(a).
I There exists: a proof of 9 x (j(x)) is given by a pair
consisting of an object a and a proof of j(a).
The Law of Excluded Middle (LEM) 8p (p _¬p) is a classical
tautology (has truth-value true), but is rejected by constructivists.
Slide 83
6.1 Intuitionistic logics
The constructivist approach to logic is outlined on Slide 83. Constructivists reject the Law of
Excluded Middle 8p (p_¬p) (as well as some other logical principles that are classically valid)
and consequently some classically valid proofs are not constructive: see Slide 84. The proof
of the theorem on that slide does not give us an example of irrational numbers a and b for
which ba is rational. Slide 85 gives a constructively valid proof of the same theorem (due to
Thierry Coquand, I think). It is certainly preferable to the previous proof, because we get more
information. This is typical: even if you accept the validity of LEM (and other non-constructive
principles of classical mathematics), constructive proofs can be more interesting and useful.
6 PROPOSITIONS AS TYPES 68
Example of a non-constructive proof
Theorem. There exist two irrational numbers a and b such that
ba is rational.
Proof. Either
p
2
p
2 is rational, or it is not (LEM!).
If it is, we can take a = b =
p
2, since
p
2 is irrational by a
well-known theorem attributed to Euclid.
If it is not, we can take a =
p
2 and b =
p
2
p
2, since then
ba = (
p
2
p
2)
p
2 =
p
2
p
2.
p
2 =
p
22 = 2.
QED
Slide 84
Example of a constructive proof
Theorem. There exist two irrational numbers a and b such that
ba is rational.
Proof.
p
2 is irrational by a well-known constructive proof
attributed to Euclid.
2 log2 3 is irrational, by an easy constructive proof (exercise).
So we can take a = 2 log2 3 and b =
p
2, for which we have that
ba = (
p
2)2 log2 3 = (
p
22)log2 3 = 2log2 3 = 3 is rational.
QED
Slide 85
For the Dutch mathematician Brouwer (1881–1966), constructivism meant rejecting truth in
some Platonic objective reality in favour of subjective mental constructions – human intuition.
For that reason his approach was called intuitionistic mathematics and the logical systems that
his follower Heyting (1898–1980) and others devised to formalize Brouwer’s ideas are called
intuitionistic logics. An example of an intuitionistic logic is given on Slides 86 and 87 – the
second-order intuitionistic propositional calculus (2IPC). The rules for generating proofs in 2IPC
involving its two constructs � and 8 come in pairs: rules for introducing the logical construct
6 PROPOSITIONS AS TYPES 69
(�I)/(8I), and rules for eliminating them (�E)/(8E). This way of organising proof rules is
called Natural Deduction and is due to the logician Gentzen (1909–1945).
Second-order intuitionistic
propositional calculus (2IPC)
2IPC propositions: f ::= p | f � f | 8p (f) where p ranges
over an infinite set of propositional variables.
2IPC sequents: F ` f where F is a finite multiset (=
unordered list) of 2IPC propositions and f is a 2IPC proposition.
F ` f is provable if it is in the set of sequents inductively
generated by:
(Id) F ` f if f 2 F
F, f ` f0
(�I)
F ` f � f0
F ` f � f0 F ` f
(�E)
F ` f0
F ` f
(8I) if p /2 fv(F)
F ` 8p (f)
F ` 8p (f)
(8E)
F ` f[f0/p]
Slide 86
A 2IPC proof
Writing p ^ q as an abbreviation for 8r ((p � q � r)� r), the
sequent
{} ` 8p (8q ((p ^ q)� p))
is provable in 2IPC:
(Id)
{p ^ q, p, q} ` p
(�I)
{p ^ q, p} ` q � p
(�I)
{p ^ q} ` p � q � p
(Id)
{p ^ q} ` 8r ((p � q � r)� r)
(8E)
{p ^ q} ` (p � q � p)� p
(�E)
{p ^ q} ` p
(�I)
{} ` (p ^ q)� p
(8I)
{} ` 8q ((p ^ q)� p)
(8I)
{} ` 8p (8q ((p ^ q)� p))
Slide 87
6.2 Curry-Howard correspondence
Computer scientists naturally take the intuitionistic notion of construction as having something
to do with the notion of algorithm from computation theory. They are interested in construc-
6 PROPOSITIONS AS TYPES 70
tive proof and intuitionistic logics because of their connections with computation. The Curry-
Howard correspondence, outlined on Slide 88 helps to formalize the connection. To see how
the Curry-Howard correspondence works, we will look at a specific instance, namely the cor-
respondence between 2IPC (Slide 86) and the PLC type system of Section 4.
Curry-Howard correspondence
Logic $ Type system
propositions f $ types t
proofs p $ expressions M
‘p is a proof of f’ $ ‘M is an expression of type t’
simplification of proofs $ reduction of expressions
E.g.
2IPC $ PLC
Slide 88
Mapping 2IPC proofs to PLC expressions
(Id) F, f ` f 7! (id) x : F, x : f ` x : f
(�I)
F, f ` f0
F ` f � f0
7! (fn)
x : F, x : f ` M : f0
x : F ` lx : f (M) : f � f0
(�E)
F ` f � f0
F ` f
F ` f0
7! (app)
x : F ` M1 : f � f0
x : F ` M2 : f
x : F ` M1 M2 : f0
(8I)
F ` f
F ` 8p (f)
7! (gen)
x : F ` M : f
x : F ` Lp (M) : 8p (f)
(8E)
F ` 8p (f)
F ` f[f0/p]
7! (spec)
x : F ` M : 8p (f)
x : F ` M f0 : f[f0/p]
Slide 89
6 PROPOSITIONS AS TYPES 71
The proof of the 2IPC sequent
{} ` 8p (8q ((p ^ q)� p))
given before is transformed by the mapping of 2IPC proofs to PLC
expressions to
{} ` Lp, q (lz : p ^ q (z p (lx : p, y : q (x))))
: 8p (8q ((p ^ q)� p))
with typing derivation:
(id)
{z : p ^ q, x : p, y : q} ` x : p
(fn)
{z : p ^ q, x : p} ` ly : q (x) : q � p
(fn)
{z : p ^ q} ` lx : p, y : q (x) : p � q � p
(id)
{z : p ^ q} ` z : 8r ((p � q � r)� r)
(spec)
{z : p ^ q} ` z p : (p � q � p)� p
(app)
{z : p ^ q} ` z p (lx : p, y : q (x)) : p
(fn)
{} ` lz : p ^ q (z p (lx : p, y : q (x))) : (p ^ q)� p
(gen)
{} ` Lq (lz : p ^ q (z p (lx : p, y : q (x)))) : 8q ((p ^ q)� p)
(gen)
{} ` Lp, q (lz : p ^ q (z p (lx : p, y : q (x)))) : 8p, q ((p ^ q)� p)
Slide 90
Logical operations definable in 2IPC
I Truth > , 8p (p � p)
I Falsity ? , 8p (p)
I Conjunction f ^ y , 8p ((f � y � p)� p)
(where p /2 fv(f, y))
I Disjunction f _ y , 8p ((f � p)� (y � p)� p) (where
p /2 fv(f, y))
I Negation ¬f , f �?
I Bi-implication f $ y , (f � y)^ (y � f)
I Existential quantification 9 p (f) , 8q (8p (f � q)� q)
(where q /2 fv(f, p))
LEM 8p (p _¬p) = 8p, q ((p � q)� ((p � 8r (r))� q)� q)
Fact: {} ` M : 8p (p _¬p) is not provable in PLC for any
expression M.
Slide 91
If we identify propositional variables with PLC’s type variables, then 2IPC propositions are
just PLC types. Every proof of a 2IPC sequent F ` f can be described by a PLC expression
M satisfying G ` M : f, once we have fixed a labelling G = {x1 : f1, . . . , xn : fn} of the
propositions in F = {f1, . . . , fn} with variables x1, . . . , xn. M is built up by recursion on the
structure of the proof of the sequent using the transformations on Slide 89. (On that slide we
abbreviate {x1 : f1, . . . , xn : fn} as x : F.) This is illustrated on Slide 90. The example on that
slide uses the fact that the logical operation of conjunction can be defined in 2IPC. Slide 91
gives some other logical operators that are definable in 2IPC. Compare it with what we saw
6 PROPOSITIONS AS TYPES 72
in Sections 4.4 and 4.5: the richness of PLC for expressing datatypes is mirrored under the
Curry-Howard correspondence by the richness of 2IPC for expressing logical connectives and
quantifiers. As one might expect from its name, in 2IPC these connectives and quantifiers
behave constructively rather than classically. For example, the Law of Excluded Middle is not
provable in 2IPC (Slide 91). This fact can be proved using the technique developed in Tripos
question 2000.9.13, which is part of the very interesting topic of the model theory (denotational
semantics) of PLC – a topic beyond the scope of these lectures.
The correspondence between PLC types/expressions and 2IPC propositions/proofs allows
one to transfer the PLC notion of computation (beta-reduction) to a notion of computation on
2IPC proofs, namely proof simplification. Slide 92 shows how the PLC beta-reduction
(lx : f (M)) N ! M[N/x]
corresponds to a simplification of 2IPC proofs in which a use of the proof rule (�I) immedi-
ately followed by a use of (�E) is eliminated. Similarly, the other form of PLC beta-reduction
(Lp (M)) f! M[f/p]
corresponds to a proof simplification of the form
…
F ` f
(8I) p /2 fv(F)
F ` 8p (f)
(8E)
F ` f[y/p]
7!
…
F ` f
(spec) p /2 fv(F)
F ` f[y/p]
where the rule (spec) is admissible in the sense described on Slide 92: one can show that if
F ` f is provable in 2IPC and p /2 fv(F),then F ` f[y/p] is also provable. Finally, note that
the Strong Normalization property for PLC (Slide 55) implies that if we repeatedly simplify a
2IPC proof we eventually reach a proof in normal form containing no (�I)–(�E) or (8I)–(8E)
pairs.
Proof simplification$ Expression reduction
…
F, f ` y
(�I)
F ` f � y
…
F ` f
(�E)
F ` y
7!
…
x : F, x : f ` M : y
x : F ` lx : f (M) : f � y
…
x : F ` N : f
x : F ` (lx : f (M)) N : y
simplify proof
????y
????y
beta-reduce expression
…
F, f ` y
…
F ` f
(cut)
F ` y
[
…
x : F, x : f ` M : y
…
x : F ` N : f
(subst)
x : F ` M[N/x] : y
The rule (subst) for PLC is admissible: if its hypotheses are valid PLC
typing judgements, then so is its conclusion.
Hence, the rule (cut) is admissible for 2IPC.
Slide 92
6 PROPOSITIONS AS TYPES 73
The Curry-Howard correspondence gives us a different perspective on the typing judge-
ment G ` M : s, outlined on Slide 93. The correspondence cuts both ways: in one direc-
tion it has proved very helpful to use typed lambda terms as notations for proofs and their
type systems in proof-search mode as part of interactive theorem-proving systems such as
Coq (coq.inria.fr) and Agda (wiki.portal.chalmers.se/agda/agda.php). In the other di-
rection, the Curry-Howard correspondence has helped to suggest new type systems for pro-
gramming and specification languages, based on various kinds of logic. Two examples of this
kind of application are the transfer of ideas from Girard’s linear logic Girard (1987) into systems
of linear types in usage analyses (see Chirimar et al. (1996)) and language-based security (see
Gaboardi et al. (2013)); and the use of type systems based on modal logics for analysing partial
evaluation and run-time code generation Davis and Pfenning (1996).
Type-inference versus proof search
Type-inference: given G and M, is there a type t such that
G ` M : t?
(For PLC/2IPC this is decidable.)
Proof-search: given G and f, is there a proof term M such that
G ` M : f?
(For PLC/2IPC this is undecidable.)
Slide 93
6.3 Calculus of Constructions, lC
2IPC is a logic of propositions (properties without any parameters) rather than predicates (prop-
erties of individuals of some type). The Curry-Howard correspondence applies to predicate
logics as well as propositional logics. Here we take a brief look at a higher-order intuitionistic
predicate logic where, among other things, one can universally quantify over individuals of a
particular type and where the collection of these types of individuals is closed under formation
of function types (this is why the logic is called higher-order). The typed lambda calculus cor-
responding to this under Curry-Howard is the Calculus of Constructions of Coquand and Huet
(1988). If can be specified as a Pure Type System lC: see Slide 94.
6 PROPOSITIONS AS TYPES 74
Calculus of Constructions
is the Pure Type System lC, where C = (SC,AC,RC) is the
PTS specification with
SC ,{Prop, Set} (Prop = a sort of propositions, Set = a sort of types)
AC ,{(Prop, Set)} (Prop is one of the types)
RC ,{(Prop, Prop, Prop)1, (Set, Prop, Prop)2,
(Prop, Set, Set)3, (Set, Set, Set)4}
1. Prop has implications, f � y = Px : f (y) (where f, y : Prop and
x /2 fv(y)).
2. Prop has universal quantifications over elements of a type, Px : A (f(x))
(where A : Set and x : A ` f(x) : Prop).
N.B. A might be Prop (l2 ✓ lC).
3. Set has types of function dependent on proofs of a proposition,
Px : p (A(x)) (where p : Prop and x : p ` A(x) : Set).
4. Set has dependent function types, Px : A (B(x)) (where A : Set and
x : A ` B(x) : Set).
Slide 94
Some general properties of lC
I It extends both l2 (PLC) and lw (Fw).
I lC is strongly normalizing.
I Type-checking and typeability are decidable.
I lC is logically consistent (relative to the usual foundations of
classical mathematics), that is, there is no pseudo-term t
satisfying ⇧ ` t : Pp : Prop (p).
Indeed there is no proof of LEM (Pp : Prop (¬p _ p)).
Slide 95
Slide 95 gives some properties of lC. The expressivity of the Calculus of Constructions
goes well beyond PLC and Fw. For example, the ability to quantify over predicates allows one
to define equality predicates for each type using a technique that goes back to Leibniz; see
Slide 96. It is possible, in principle, to express a lot of constructive mathematics within lC. It
was the starting point for the Coq theorem-proving system (coq.inria.fr). Compared with
classical higher-order predicate logic (Church, 1940), lC is a proof-relevant logic: it is possible
to express constructions on proofs of propositions as well as on elements of types (cf. item 3
on Slide 94).
6 PROPOSITIONS AS TYPES 75
Leibniz equality in lC
Gottfried Wilhelm Leibniz (1646–1716),
identity of indiscernibles:
duo quaedam communes proprietates eorum nequaquam possit
(two distinct things cannot have all their properties in common).
Given G ` A : Set in lC, we can define
EqA , lx, y : A (PP : A � Prop (P x $ P y))
satisfying G ` EqA : A � A � Prop and giving a well-behaved (but
not extensional) equality predicate for elements of type A.
Slide 96
Extensionality
Functional extensionality:
FunExtA,B , P f , g : A � B (
(Px : A (EqB ( f x) (g x)))� EqA�B f g)
If G ` A, B : Set in lC, then G ` FunExtA,B : Prop is derivable,
but for some A,B there does not exist a pseudo-term t for which
G ` t : FunExtA,B is derivable.
Propositional extensionality:
PropExt , Pp, q : Prop ((p $ q)� Eq
Prop
p q)
⇧ ` PropExt : Prop is derivable in lC, but there does not exist a
pseudo-term t for which ⇧ ` t : PropExt is derivable.
Slide 97
The universe Prop of propositions in lC is said to be impredicative, because in order to
construct a proposition, we are allowed to quantify over all propositions (as on Slide 91), in-
cluding the one we are trying to construct! That the collection of all subsets of a set is itself a
set is a similar form of impredicativity and strict constructivists do not admit the existence of
powersets, even though their use is widespread in every day mathematics. lC is also inten-
sional in the sense that it fails to validate the well-known principle of function extensionality, or
the less well-known one of propositional extensionality (Slide 97). The latter is a special case of
6 PROPOSITIONS AS TYPES 76
Voevodsky’s Univalence Axiom, part of Homotopy Type Theory (Univalent Foundations Program,
2013), a topic which is currently under very active development.
The Pure Type System lU
is given by the PTS specification U = (SU,AU,RU), where:
SU , {Prop, Set, Type}
AU , {(Prop, Set), (Set, Type)}
RU , {(Prop, Prop, Prop), (Set, Prop, Prop), (Type, Prop, Prop),
(Set, Set, Set), (Type, Set, Set)}
Theorem (Girard). lU is logically inconsistent: every legal
proposition G ` P : Prop has a proof G ` M : P. (In particular,
there is a proof of falsity ? , Pp : Prop (p).)
Slide 98
6.4 Inductive types
We saw in Section 4.4 how PLC’s (impredicative!) ability to quantify over all types when form-
ing type expressions can be used to represent algebraic data types as PLC types. PLC, viewed
as the Pure Type System l2, is a subsystem of the Calculus of Constructions, lC. This casts PLC
as the language of proofs of the logic 2IPC within lC: its types become propositions (pseudo-
terms of sort Prop), not types (pseudo-terms of sort Set). So for example the polymorphic nat-
ural numbers 8a (a � (a � a)� a) becomes a proposition ⇧ ` Pp : Prop (p � (p � p)� p) : Prop
that is provable in countably many different ways (given by the countably many different nor-
mal forms of that type). As far as proof-search (Slide 93) is concerned, there is not much to
choose between Pp : Prop (p � (p � p) � p) and Pp : Prop (p � p), since both are provable.
Can we use this kind of impredicative encoding of algebraic data types to produce lC types,
rather than propositions? Not as it stands: the pseudo-term Px : Set (x � (x � x) � x) is not
legal in lC (exercise). To make it legal one can extend lC with a sort Type for ‘big’ types (in
particular Set : Type), enabling one to add a PTS specification rule (Type, Set, Set) expressing
that the sort Set, like Prop, is closed under forming impredicative P-types. This extension of
lC is the PTS known as lU, described on Slide 98.
The theorem on Slide 98, due to Girard (1972), shows that lU is not useful as a logic.
A similiar, but slightly easier result holds for the PTS l⇤ mentioned on Slide 76. These re-
sults are known as Girard’s Paradox and are a type-theoretic version of the Burali-Forti set-
theoretic paradox; see Coquand (1986) and Barendregt (1992, Section 5.5). If one wishes to use
dependently-typed lambda calculi as the basis of theorem-proving systems, then they had bet-
ter correspond under Curry-Howard to consistent logical systems. So lU and l⇤ are not useful
from that point of view. They are of interest from a programming-language point of view, but
the impredicative encodings of data types that they admit really are of theoretical rather than
practical interest: when using such representations, some standard functions can be hard to
6 PROPOSITIONS AS TYPES 77
program (for example, subtraction of numbers) and/or computationally inefficient. Instead,
one can just extend lC with syntax and reductions that directly (rather than impredicatively)
express such data types, following the pattern on Slide 99.
Inductive types (informally)
An inductive type is specified by giving
I constructor functions that allow us to inductively generate
data values of that type
(Some restrictions on how the inductive type appears in the domain type
of constructors is needed to ensure termination of reduction and logical
consistency.)
I eliminators for constructing functions on the data
I computation rules that explain how to simplify an eliminator
applied to constructors.
Slide 99
Extending lC with
an inductive type of natural numbers
Pseudo-terms
t ::= · · · | Nat | zero | succ | elimNat(x.t) t t
Typing rules
I formation: ⇧ ` Nat : Set
I introduction: ⇧ ` zero : Nat ⇧ ` succ : Nat � Nat
I elimination:
G, x : Nat ` A(x) : s G ` M : A(zero)
G ` F : Px : Nat (A(x)� A(succ x))
G ` elimNat(x.A) M F : Px : Nat (A(x))
(where A(t) stands for A[t/x])
Computation rules
elimNat(x.A) M F zero ! M
elimNat(x.A) M F (succ N) ! F N (elimNat(x.A) M F N)
Slide 100
Slide 100 gives the simple example of extending Calculus of Constructions with an induc-
tive type of natural numbers. The pseudo-terms zero and succ are the constructors for the
inductively defined type Nat and the pseudo-terms elimNat(x.A) M F are its eliminators. The
6 PROPOSITIONS AS TYPES 78
elimination typing rule in case the sort s is Set gives a dependently-typed version of prim-
itive recursive functions (cf. the CST IB Computation Theory course). For example addition
⇧ ` add : Nat � Nat � Nat is given by
add , lx : Nat (elimNat(y. Nat) x (ly : Nat (succ))) (11)
for which the computation rules on Slide 100 yield
add x zero!⇤ x (12)
add x (succ y)!⇤ succ(add x y). (13)
Furthermore, the elimination typing rule in case the sort s is Prop yields, under the Curry-
Howard correspondence, a version of the usual principle of mathematical induction
F ` f(zero) F ` 8x : Nat (f(x)� f(succ x))
F ` 8x : Nat (f(x))
(14)
This is typical of the Curry-Howard correspondence for inductive types in a dependently-
typed setting: definition by structural recursion and proof by structural induction are two sides of
the same coin, given by the eliminator and its computation rules.
An important consequence of working with dependently-typed systems is that one can
consider inductive definitions of whole indexed families of data types with dependently-typed
constructor functions: the particular type of data constructed can depend upon the type of the
argument to which the constructor is applied. Slides 101 and 102 give two examples. Many
more examples can be found in the book by Nordström et al. (1990). The article by Oury and
Swierstra (2008) is a nice illustration of the usefulness of dependently-typed inductive types in
functional programming, making use of Agda.
Inductive types of vectors
For a fixed parameter G ` A : s, the indexed family
(VecA x | x : Nat) of types VecA x of lists of A-values of length
x is inductively defined as follows:
Formation:
G ` N : Nat
G ` VecA N : Set
Introduction:
G ` vnilA : VecA zero
G ` vconsA : A � Px : Nat (VecA x � VecA (succ x))
Elimination and Computation:
[do-it-yourself]
Slide 101
6 PROPOSITIONS AS TYPES 79
Inductive identity propositions
For fixed parameters G ` A : s and G ` a : A, the indexed family
(IdA,a x | x : A) of propositions IdA,a x that a and x are equal
elements of type A is inductively defined as follows:
Formation:
G ` M : A
G ` IdA,a M : Prop
Introduction:
G ` reflA,a : IdA,a a
Elimination:
G, x : A, p : IdA,a x ` B(x, p) : s G ` N : B(a, reflA,a)
G ` JA,a(x, p. B) N : Px : A (Pp : IdA,a x (B(x, p)))
Computation:
JA,a(x, p. B) N a reflA,a ! N
Slide 102
Agda proof of 8x 2 N (x = 0 + x)
data Nat : Set where
zero : Nat
succ : Nat -> Nat
add : Nat -> Nat -> Nat
add x zero = x
add x (succ y) = succ (add x y)
data Id (A : Set)(x : A) : A -> Set where
refl : Id A x x
cong : (A B : Set)(f : A -> B)(x y : A) ->
Id A x y -> Id B (f x) (f y)
cong A B f x .x refl = refl
P : (x : Nat) -> Id Nat x (add zero x)
P zero = refl
P (succ x) = cong Nat Nat succ x (add zero x) (P x)
Slide 103
Both Agda and Coq allow the user to define their own inductive types; arguably, this is
their most useful feature. The theoretical basis for this is the fact that it is possible to automatically
generate elimination and computation rules from user-supplied formation and introduction rules for a
given inductive type (Coquand and Paulin, 1990). However, writing functions on inductive data
in terms of eliminators rapidly becomes very unmanageable. For example, if lC is extended
with a type of natural numbers as on Slide 100 and with equality propositions as on Slide 102,
then it is possible, but rather tedious, to construct a pseudo-term P satisfying
⇧ ` P : Px : Nat (Id
Nat,x(add zero x)) (15)
6 PROPOSITIONS AS TYPES 80
in other words, to construct a proof (by induction!) of the trivial proposition 8x 2 N (x = 0 + x)
(exercise).10 Instead, both Coq and Agda support fixed point definitions involving case-by-
case matching of data to constructor patterns, similar to the kind of definitions allowed by
languages in the ML family and in Haskell.11 For example, the proof of (15) in Agda is shown
on Slide 103.
Uniqueness of identity proofs
In lC extended with inductive identity propositions, there are
some types G ` A : s for which it is impossible to prove that all
equality proofs in IdA,x y (where x, y : A) are identical.
That is, there is no pseudo-term uip satisfying
G ` uip : Px, y : A (Pp, q : IdA,x y (Id(IdA,x y),p q))
By contrast, in Agda we have:
data Id (A : Set)(x : A) : A -> Set where
refl : Id A x x
uip : (A : Set)(x y : A)(p q : Id A x y) -> Id (Id A x y) p q
uip A x .x refl refl = refl
Slide 104
Pattern-matching in a dependently-typed setting is more involved than in the simply-
typed case. For example the Agda definition of cong on Slide 103 matches expressions of
type Id A x y against the constructor pattern refl; since this has type Id A x y only when x
and y are the same, the defining clause for cong replaces y by an ‘inaccessible’ pattern .x that
is determined by the pattern variable x. What is being implemented by Agda is the pattern-
matching algorithm for dependent types due to Coquand (1992); see (Norell, 2007, Chapter 2)
for a user-oriented discussion of this. It turns out to be strictly more expressive than algo-
rithms that elaborate patterns into eliminator forms; see Slide 104. The impossibility of prov-
ing uniqueness of identity proofs from the rules on Slide 102 is a model-theoretic argument
due to Hofmann and Streicher (1998). Recent versions of Agda use the work of Cockx et al.
(2014) to optionally constrain pattern-matching to make proofs like the one at the bottom of
Slide 104 impossible.
10Note that the symmetric version 8x 2 N (x = x + 0) can be proved merely by calculation: by (12), Px :
Nat (Id
Nat,x(add x zero)) reduces to Px : Nat (IdNat,x x), which is inhabited by reflNat,x.
11One difference is that syntactic restrictions are placed on occurrences of the defined function in the fixed point
definition in order to ensure termination of reduction and logical consistency.
7 FURTHER TOPICS 81
7 Further Topics
The study of types forms a very vigorous area of computer science research, both for comput-
ing theory and in the application of theory to practice. This course has aimed at reasonably
detailed coverage of a few selected topics, centred around the notion of polymorphism in pro-
gramming languages and the propositions-as-type paradigm. The book Pierce (2005) is a good
source for essays on further topics in type systems for programming languages.
References
Aho, A. V., R. Sethi, and J. D. Ullman (1986). Compilers. Principles, Techniques, and Tools. Addison Wesley.
Aspinall, D. and M. Hofmann (2005). Dependent types. In B. C. Pierce (Ed.), Advanced Topics in Types
and Programming Languages, Chapter 2, pp. 45–86. The MIT Press.
Augustsson, L. (1998). Cayenne–a language with dependent types. In ACM SIGPLAN International
Conference on Functional Programming, ICFP 1998, Baltimore,Maryland, USA. ACM Press.
Barendregt, H. P. (1992). Lambda calculi with types. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum
(Eds.), Handbook of Logic in Computer Science, Volume 2, pp. 117–309. Oxford University Press.
Barthe, G. (1999). Type-checking injective pure type systems. Journal of Functional Programming 9(6),
675–698.
Bove, A. and P. Dybjer (2009). Dependent types at work. In Language Engineering and Rigorous Software
Development, pp. 57–99. Springer.
Cardelli, L. (1987). Basic polymorphic typechecking. Science of Computer Programming 8, 147–172.
Cardelli, L. (1997). Type systems. In CRC Handbook of Computer Science and Engineering, Chapter 103,
pp. 2208–2236. CRC Press.
Chirimar, J., C. A. Gunter, and J. G. Riecke (1996). Reference counting as a computational interpretation
of linear logic. Journal of Functional Programming 6(2), 195–244.
Church, A. (1940). A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68.
Cockx, J., D. Devriese, and F. Piessens (2014). Pattern matching without K. In Proceedings of the 19th
ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, New York, NY, USA,
pp. 257–268. ACM.
Coquand, T. (1986, June). An analysis of girard’s paradox. In Proceedings of the First Annual IEEE
Symposium on Logic in Computer Science (LICS 1986), pp. 227–236. IEEE Computer Society Press.
Coquand, T. (1992, June). Pattern matching with dependent types. In B. Nordström, K. Petersson, and
G. D. Plotkin (Eds.), Proceedings of the 1992 Workshop on Types for Proofs and Programs, Båstad, Sweden,
pp. 66–79.
Coquand, T. and G. Huet (1988). The calculus of constructions. Information and Computation 76(2–3),
95–120.
Coquand, T. and C. Paulin (1990). Inductively defined types. In P. Martin-LÃűf and G. Mints (Eds.),
COLOG-88, Volume 417 of Lecture Notes in Computer Science, pp. 50–66. Springer Berlin Heidelberg.
Damas, L. and R. Milner (1982). Principal type schemes for functional programs. In Proc. 9th ACM
Symposium on Principles of Programming Lanuages, pp. 207–212.
Davis, R. and F. Pfenning (1996). A modal analysis of staged computation. In ACM Symposium on
Principles of Programming Languages, St. Petersburg Beach, Florida, pp. 258–270. ACM Press.
de Bruijn, N. G. (1970). The mathematical language automath, its usage, and some of its extensions. In
M. Laudet, D. Lacombe, L. Nolin, and M. SchÃijtzenberger (Eds.), Symposium on Automatic Demon-
stration, Volume 125 of Lecture Notes in Mathematics, pp. 29–61. Springer Berlin Heidelberg.
Gaboardi, M., A. Haeberlen, J. Hsu, A. Narayan, and B. C. Pierce (2013). Linear dependent types for
differential privacy. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles
of Programming Languages, POPL ’13, New York, NY, USA, pp. 357–370. ACM.
Girard, J.-Y. (1972). Interprétation fonctionelle et élimination des coupures dans l’arithmetique d’ordre supérieur.
Ph. D. thesis, Université Paris VII. Thèse de doctorat d’état.
82
REFERENCES 83
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50, 1–101.
Girard, J.-Y. (1989). Proofs and Types. Cambridge University Press. Translated and with appendices by
Y. Lafont and P. Taylor.
Gordon, M. J. C. and T. F. Melham (1993). Introduction to HOL. A Theorem Proving Environment for Higher
Order Logic. Cambridge University Press.
Harper, R. (1994). A simplified account of polymorphic references. Information Processing Letters 51,
201–206.
Harper, R. and C. Stone (1997). An interpretation of Standard ML in type theory. Technical Report
CMU–CS–97–147, Carnegie Mellon University, Pittsburgh, PA.
Hindley, J. R. (1969). The principal type scheme of an object in combinatory logic. Transations of the
American Mathematical Society 146, 29–40.
Hofmann, M. and T. Streicher (1998). The groupoid interpretation of type theory. In G. Sambin (Ed.),
Twenty-Five Years of Constructive Type Theory, Volume 36 of Oxford Logic Guides, pp. 83–111. Oxford
University Press.
Lamport, L. and L. C. Paulson (1999). Should your specification language be typed? ACM Transactions
on Programming Languages and Systems 21(3), 502–526.
MacLane, S. (1971). Categories for the Working Mathematician. Graduate Texts in Mathematics 5. Springer.
Mairson, H. G. (1990). Deciding ML typability is complete for deterministic exponential time. In Proc.
17th ACM Symposium on Principles of Programming Languages, pp. 382–401. ACM Press.
Martin-Löf, P. (1975). An intuituionistic theory of types: Predicative part. In H. E. Rose and J. C.
Shepherdson (Eds.), Logic Colloquium ’73, pp. 73–118. North-Holland.
Milner, R., M. Tofte, and R. Harper (1990). The Definition of Standard ML. MIT Press.
Milner, R., M. Tofte, R. Harper, and D. MacQueen (1997). The Definition of Standard ML (Revised). MIT
Press.
Mitchell, J. C. (1996). Foundations for Programming Languages. Foundations of Computing series. MIT
Press.
Mitchell, J. C. and G. D. Plotkin (1988). Abstract types have existential types. ACM Transactions on
Programming Languages and Systems 10, 470–502.
Nordström, B., K. Petersson, and J. M. Smith (1990). Programming in Martin-Löf’s Type Theory. Oxford
University Press.
Norell, U. (2007, September). Towards a Practical Programming Language Based on Dependent Type Theory.
Ph. D. thesis, Department of Computer Science and Engineering, Chalmers University of Technology,
SE-412 96 Göteborg, Sweden.
Oury, N. and W. Swierstra (2008). The power of pi. In Proceedings of the 13th ACM SIGPLAN International
Conference on Functional Programming, ICFP ’08, New York, NY, USA, pp. 39–50. ACM.
Peyton Jones, S. L. (2001). Tackling the awkward squad: Monadic input/output, concurrency, excep-
tions, and foreign-language calls in Haskell. In A. Hoare, M. Broy, and R. Steinbruggen (Eds.), Engi-
neering Theories of Software Construction, pp. 47–96. IOS Press.
Pierce, B. C. (2002). Types and Programming Languages. MIT Press.
Pierce, B. C. (Ed.) (2005). Advanced Topics in Types and Programming Languages. MIT Press.
REFERENCES 84
Rémy, D. (2002). Using, understanding, and unravelling the ocaml language: From practice to theory
and vice versa. In G. Barthe, P. Dybjer, and J. Saraiva (Eds.), Applied Semantics, Advanced Lectures,
Volume 2395 of Lecture Notes in Computer Science, Tutorial, pp. 413–537. Springer-Verlag. International
Summer School, APPSEM 2000, Caminha, Portugal, September 9–15, 2000.
Reynolds, J. C. (1974). Towards a theory of type structure. In Paris Colloquium on Programming, Vol-
ume 19 of Lecture Notes in Computer Science, pp. 408–425. Springer-Verlag, Berlin.
Robinson, J. A. (1965). A machine oriented logic based on the resolution principle. Journal of the ACM 12,
23–41.
Russell, B. (1903). The Principles of Mathematics. Cambridge.
Rydeheard, D. E. and R. M. Burstall (1988). Computational Category Theory. Series in Computer Science.
Prentice Hall International.
Strachey, C. (1967). Fundamental concepts in programming languages. Lecture notes for the Interna-
tional Summer School in Computer Programming, Copenhagen.
Tofte, M. (1990). Type inference for polymorphic references. Information and Computation 89, 1–34.
Tofte, M. and J.-P. Talpin (1997). Region-based memory management. Information and Computa-
tion 132(2), 109–176.
Univalent Foundations Program, T. (2013). Homotopy Type Theory: Univalent Foundations for Mathematics.
Institute for Advanced Study: http://homotopytypetheory.org/book.
Wadler, P. (1992). Comprehending monads. Mathematical Structures in Computer Science 2, 461–493.
Wells, J. B. (1994). Typability and type-checking in the second-order l-calculus are equivalent and
undecidable. In Proceedings, 9th Annual IEEE Symposium on Logic in Computer Science, Paris, France,
pp. 176–185. IEEE Computer Society Press.
Wright, A. K. (1995). Simple imperative polymorphism. LISP and Symbolic Computation 8, 343–355.
Wright, A. K. and M. Felleisen (1994). A syntactic approach to type soundness. Information and Compu-
tation 115, 38–94.
Xi, H. and F. Pfenning (1998). Eliminating array bound checking through dependent types. In Proc.
ACM-SIGPLAN Conference on Programming Language Design and Implementation, Montreal, Canada, pp.
249–257. ACM Press.