Exercise 4: Simply Typed Lambda Calculus Extensions
Hand in: Dec. 15 (Friday).
Change: We have extended the deadline
so that the hand in is after next lecture, where recursion is presented.
In this exercise, we reuse the combinator parsing library introduced
in exercise 1.
Assignment
In this assignment you will extend your simply typed lambda
calculus project from exercise 3 with
sum types and recursive functions.
Sum Types
Sum types are handy when one needs to handle heterogeneous
collections of values.
Imagine you have a data type like a tree, where each element can be a
leaf (containing a value) or an inner node (containing two references
to subtrees). A sum type is a type which draws its values from exactly
two other types. In other words, values of a sum type
T1 + T2 can be either of type
T1 or of type T2.
We introduce now syntactic rules for sum types, together with
evluation and typing rules.
| t |
::= .. |
|
terms |
|
| |
"inl" t "as" T |
inject left |
|
|
| |
"inr" t "as" T |
inject right |
|
|
| |
"case" t "of" "inl" x "=>" t "|" "inr" x "=>" t |
case |
|
| v |
::= .. |
|
values |
|
| |
"inl" v "as" T |
|
| |
"inr" v "as" T |
| T |
::= .. |
|
types |
|
|
| |
T "+" T |
sum
type (right associative) |
|
We create values of a sym type by injecting a value in
the "left" or right "part". To deconstruct such values, we use a
case expression, similar to Scala's match construct.
Sum types are right associative and + has the same precedence
as *.
case (inl v0) of
inl x1 => t1 | inr x2 => t2
→ [x1 ↦ v0]t1 |
|
case (inr v0) of
inl x1 => t1 | inr x2 => t2
→ [x2 ↦ v0]t2 |
|
| t → t' |
| case t of inl x1 => t1 | inr x2 => t2
→ case t' of inl x1 => t1 | inr x2 => t2 |
|
|
|
|
|
And last, the additional typing rules are:
|
Γ|— t1: T1
|
|
Γ|— inl
t1 as T1 + T2 : T1 + T2
|
|
|
Γ|— t1: T2
|
|
Γ|— inr
t1 as T1 + T2 : T1 + T2
|
|
Γ|—
t0: T1+T2
Γ, x1: T1|—
t1: T
Γ, x2: T2|—
t2: T
|
|
Γ|—
case t0 of inl x1 =>
t1 | inr x2 => t2 : T
|
|
Evaluation and typing rules are pretty straight forward, the
only thing a bit out of ordinary is the type adornment for
inl and inr. This is necessary because the two
constructors can't possibly know what is the type of the other
component of the sum type. By giving it explicitly, the type
checker is able to proceed. Alternatives to this decision will
be explored in other exercises, when we know about type
inference.
The fix operator
To bring back the fun into the game, we need some way to write
non terminating programs (or at least, looping
programs). Since types arrived, we were unable to type the
fixpoint operator, and indeed there's a theorem which states
that all well typed terms in simply typed lambda calculus
evaluate to a normal form. The only alternative is to add it
into the language.
t ::= ...
| "fix" t fixed point of t
| fix (λx: T1.t2)
→ [x ↦ (fix (λx: T1.t2))]t2 |
|
|
|
|
Γ|—
t1: T1 -> T1
|
|
Γ|— fix
t1: T1
|
|
In order to make the fixpoint operator easier to use, add the
following derived form:
letrec x: T1 = t1 in t2 => let x
= fix (λx:T1.t1) in t2
Implementation
Here is a summary of what you need to implement for this assignment:
-
Extend your parser with sum types and fix
-
A type checker which given a term finds its type (or it prints
an error message).
-
Extend the call by value reducer (small step) to account
for the new constructs.