PLDA Homework 3: Type inference

Implement type inference for expressions with the following (abstract) syntax:

Expr ::= num | var | Expr '+' Expr | if Expr then Expr else Expr | fun var -> Expr | Expr Expr
i.e., integers, variables, addition, conditional, lambda abstraction and application. The type of a free variable should be a type variable. Report invalid typing using exceptions.

Some test examples:
fun f -> fun f1 -> fun f2 -> fun s1 -> fun s2 -> fun v -> f1 (fun e1 -> f2 (f e1)) s2 s1 v
fun x0 -> fun x1 -> fun x2 -> fun x3 -> x0 (x0 x1) (x0 x1 x2) (x0 x1 x2 x3)

A parser (for the lambda calculus subset only).


Marius Minea
Last modified: Fri Oct 29 12:00:00 EET 2010