Exercise 4: Simply Typed Lambda Calculus Extensions

Hand in: November. 15 (Thursday).

In this exercise, we reuse the combinator parsing library introduced in exercise 1. The project skeleton is the same one you started with for the last assignment. You should continue working on your project, and the final submission should contain all extensions, both from this assignment and from the last assignment.

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
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
Don't forget that we implement let as a derived form as well, so the actual desugaring is a bit more complex.

Implementation

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

Input/Output

Your program should read a string from standard input until end-of-file is encountered, which represents the input program. If the program is syntactically correct, it should print its type and then print each step of the small-step reduction, starting with the input term, until it reaches a normal value. You should not worry about non-terminating programs. If there is a type error, it should print the error message and the position where it occured and skip the reduction. The provided framework already implements this behavior. You should use it as-is.

Hints