Exercise 3: Simply Typed Lambda Calculus
Hand in: Dec. 5 (2 weeks). Change:
Instead of handing in on Wednesday night,
we moved the deadline one day earlier. This way, during Wednesday
lecture and lab session we can give feedback on last week's assignment.
In this exercise, we reuse the combinator parsing library introduced
in exercise 1.
The provided framework is selfcontained and can be downloaded as
zip or
tar.gz archive.
The API documentation for this exercise is
available online.
Assignment
The goal of this exercise is to familiarize yourself with the simply typed
λcalculus; your work consists of implementing a type checker
and a reducer for simply typed λterms. To make it more
interesting, we extend lambda calculus with booleans and integers
values, let and pairs. Also, this time we'll fix a call by value
strategy, so there will be only one reducer you need to write
(actually, you can reuse some of the reducer from the previous assignment).
We first introduce the syntax for typed λcalculus without
let and pairs, which we'll add later. It might be
a good idea to start implementing this language first, and later add
the rest.
t 
::= 
"true" 
true value 


 
"false" 
false value 


 
"if" t_{1} "then" t_{2} "else" t_{3} 
if 


 
0 
zero 


 
"pred" t 
predecessor 


 
"succ" t 
successor 


 
"iszero" t 
iszero 


 
x 
variable 


 
"\" x ":" T "." t 
abstraction 


 
t t 
application 
(left associative) 

 
"(" t ")" 


v 
::= 

values 

 
"true" 

 
"false" 

 
nv 
numeric value 

 
"\" x ":" T "." t 
abstraction value 
nv 
::= 

numeric values 

 
"0" 

 
"succ" nv 
The only new thing in the above rules is the type annotation
for lambda abstractions. We see that the variable name is followed by
colon and a type. It roughly says "this function expects an argument
of type T". In the above rules, T stands for types, and here's the syntax
for types:
T 
::= 
"Bool" 
boolean type 


 
"Nat" 
numeric type 


 
T ">" T 
function types 
(right associative) 


 
"(" T ")" 


There are three kinds of types in this language: booleans, natural
numbers and function types. The type constructor ">" is
rightassociative — that is, the expression T_{1}
> T_{2} > T_{3}
stands for
T_{1} > (T_{2} > T_{3})
[TAPL, p.100].
Evaluation rules for this language are straight forward. You may note
that they already fix the evaluation strategy to call by value, and
that the type of an abstraction is ignored during evaluation. We can
say that evaluation of simply typed lambda terms proceeds exactly the
same as for untyped lambda terms. The operation of stripping off type
annotations is called erasure and it is what enabled the
addition of Java generics without modifying the virtual machine.
Computation 
Congruence 
if true then t_{1} else t_{2} → t_{1} 
if false then t_{1} else t_{2} → t_{2} 
isZero zero → true 
isZero succ NV → false 
pred zero → zero 
pred succ NV → NV 
(λx: T.t_{1}) v_{2} → [x
→ v_{2}] t_{1} 

t_{1} → t_{1}' 
if t_{1} then t_{2} else t_{3} → if t_{1}' then t_{2} else t_{3} 

t → t' 
isZero t → isZero t' 



t_{1} → t_{1}' 
t_{1} t_{2} → t_{1}' t_{2} 

t_{2} → t_{2}' 
v_{1} t_{2} → v_{1} t_{2}' 


Typing rules:



Γ— t: Nat 
Γ— pred t: Nat 

Γ— t: Nat 
Γ— succ t: Nat 

Γ— t: Nat 
Γ— iszero t: Bool 


Γ— t_{1}: Bool Γ
— t_{2}: T Γ— t_{3}: T 
Γ— if t_{1} then t_{2} else t_{3}:
T 


Γ, x: T_{1}— t: T_{2} 
Γ— λx: T_{1}.t_{2}: T_{1}
> T_{2} 

Γ— t_{1}:
T_{11}>T_{12} Γ
— t_{2}: T_{11} 
Γ— t_{1} t_{2}: T_{12}



The above typing rules define a typing relation, similar to the
evaluation relation. However, while evaluation is a relation between
terms, typing is a relation between terms, types and
contexts. A typing rule like the first one can be read "under
context gamma, term true has type Bool". The role of the
context (or environment) is to keep around a mapping between variable
names and their types. It will be used to type free variables, when
they are encountered. This is illustrated by the variable rule which
can be read "under context gamma, variable x has type T
provided context gamma has a binding for variable x to type T".
The purpose of this type system is to prevent "bad things" to
happen. So far, the only bad thing we know is stuck terms, and this
type system prevents stuck terms. In other words, a term that can be
assigned a type (it type checks) is guaranteed not to get
stuck. The result of its evaluation will be a value.
Extensions
Let us now proceed to the addition of let:
t ::= ...
 "let" x ":" T "=" t "in" t
We can define let in terms of the existing concepts, and
this has the advantage that once the translation is done in the
parser, no addition is necessary to the type checker or to the
evaluator. Such an addition is called a derived form. The
language that is accepted by our parser is called external
language and the language understood by the evaluator (and type
checker) is called internal language. And here is the
translation of let in terms of abstraction and application:
"let" x ":" T "=" t_{1} "in" t_{2} > (\x: T. t_{2}) t_{1}
To add pairs, we can't do the same trick so we'll need to extends
the existing syntax, evaluation and typing rules:
t ::= ...
 "{" t "," t "}"
 "fst" t
 "snd" t
v ::= ..
 "{" v "," v "}"
T ::= ...
 T "*" T (right associative)
The first form creates a new pair, and the other two are called
projections, and extract the first and the second element of a
pair. We add a new kind of values, pair values, and a new kind of
type, for the corresponding pair type. We decide that the pair type
constructor (denoted by *) takes precedence over the arrow
constructor, so Nat * Nat > Bool is parsed as (Nat *
Nat) > Bool.
The new evaluation rules are:
fst {v_{1}, v_{2}}
→ v_{1} 

snd {v_{1}, v_{2}}
→ v_{2} 




t_{1} → t_{1}' 
{t_{1}, t_{2}}
→ {t_{1}', t_{2}} 

t_{2} → t_{2}' 
{v_{1}, t_{2}}
→ {v_{1}, t_{2}'} 


And last, the additional typing rules:
Γ— t_{1}: T_{1}
Γ— t_{2}: T_{2}

Γ— {t_{1}, t_{2}} :
T_{1} * T_{2}


Γ— t: T_{1}*T_{2}

Γ— fst t: T_{1}


Γ— t: T_{1}*T_{2}

Γ— snd t: T_{2}


Implementation
Here is a summary of what you need to implement for this assignment:

A parser for the given grammar (including let and pairs).

A type checker which given a term finds its type (or it prints
an error message).

A call by value reducer (small step) with the corresponding
path method which gives back the stream of intermediate
terms.