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.


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
t → t'
inl t → inl t'
t → t'
inr t → inr t'

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
t → t'
fix t → fix t'
Γ|— 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


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