Exercise 4: Simply Typed Lambda Calculus Extensions
Hand in: November 10 (1 week only!)
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
T_{1} + T_{2} can be either of type
T_{1} or of type T_{2}.
We introduce now syntactic rules for sum types, together with
evaluation 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 sum 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 v_{0}) of
inl x_{1} => t_{1}  inr x_{2} => t_{2}
→ [x_{1} ↦ v_{0}]t_{1} 

case (inr v_{0}) of
inl x_{1} => t_{1}  inr x_{2} => t_{2}
→ [x_{2} ↦ v_{0}]t_{2} 

t → t' 
case t of inl x_{1} => t_{1}  inr x_{2} => t_{2}
→ case t' of inl x_{1} => t_{1}  inr x_{2} => t_{2} 



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

Γ— inl
t_{1} as T_{1} + T_{2} : T_{1} + T_{2}


Γ— t_{1}: T_{2}

Γ— inr
t_{1} as T_{1} + T_{2} : T_{1} + T_{2}


Γ—
t_{0}: T_{1}+T_{2}
Γ, x_{1}: T_{1}—
t_{1}: T
Γ, x_{2}: T_{2}—
t_{2}: T

Γ—
case t_{0} of inl x_{1} =>
t_{1}  inr x_{2} => t_{2} : 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: T_{1}.t_{2})
→ [x ↦ (fix (λx: T_{1}.t_{2}))]t_{2} 


Γ—
t_{1}: T_{1} > T_{1}

Γ— fix
t_{1}: T_{1}


In order to make the fixpoint operator easier to use, add the
following derived form:
letrec x: T_{1} = t_{1} in t_{2} => let x
= fix (λx:T_{1}.t_{1}) in t_{2}
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:

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.
Input/Output
Your program should read a string from standard input until
endoffile 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 smallstep reduction, starting with the
input term, until it reaches a normal value. You should not
worry about nonterminating 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 asis.
Hints

Don't forget to override the method
toString()
in the
subclasses of class Term
in order to get a clean output!

You should maintain positions in your abstract syntax
trees. This is done by using
positioned
around
parsers (the skeleton project already has them in place). This
method takes care of updating the position on your trees, during
parsing. Type errors should mention tree positions (have a look
at class TypeError
to see how it's done).