In this homework you should implement some of the basic concepts introduced in the first lectures. We suggest that you use Haskell or your own favourite functional programming language. It is possible to use Java or another imperative or object-oriented language, but it is much harder work!
1. Implement an evaluator for Pierce's language of arithmetic expressions! If you use Haskell you implement a data type Exp of arithmetic expressions and a data type Val of values, that is, containing the Boolean values true and false, and the number values 0, succ(0), succ(succ(0)), etc. Then you define a function
eval :: Exp -> Val
so that eval t = v iff t ->* v and v is a value according to the computation rules for arithmetic expressions.
2. Implement a type inference algorithm for arithmetic expressions! Write a function
inferType : Exp -> Maybe Type
so that
inferType t = Just T iff t : T
according to the typing rules. Otherwise,
inferType t = Nothing
The type Type contains the types Nat and Bool for arithemetic expressions. Be aware of the distinction between object and metalanguage types! The object language is the language of arithmetic expressions and the metalnaguage is Haskell, or your own favourite programming language.
3. Implement a type inference algorithm for the simply typed lambda calculus a la Church! Define a datatype LExp of lambda expressions a la Church, a type Cxt of contexts and a type LType of types (including at least Bool and funtion types). Then write a function
inferType : Cxt -> LExp -> Maybe LType
such that
inferType Gamma t = Just T iff Gamma |- t : T
according to the typing rules for the simply typed lambda calculus.
If t has no type inferType should return Nothing.
4. Why is it more difficult to implement type inference for the typed lambda calculus a la Curry? Note that such an algorithm forms the core of the type inference algorithm for polymorphic languages such as Haskell, OCaml, and SML.