#### Due on Friday, May 8th

# Implementing Type Inference

In the past two assignments, you've implemented type checking for a language with monomorphic types and explicit annotations, and you've gained some experience in working with polymorphic types and explicit annotations in a real-world programming language (Java).

In this assignment, you'll complete an implementation of Hindley/Milner type *inference*, which is the backbone of the implementation of most every language with parametric polymorphism and implicit annotation.

# Supporting Code

This is the partial implementation that I handed out in class on Friday (05/01). Your job is to complete it. Specifically, you should complete the implementations of `unify()` and `check`.

Your implementation of `unify()` should be *well-founded*, which is to say that is should refuse to produce a substitution (by raising a `CircularType` exception instead) for expressions with circular type constraints such as

val circ = (Lettrec("f",Fn("x",Variable "f"), Number 5); (* val c = let val rec f = (fn x => f) in 5 end; *)

Here are some AST objects with which you can test your work:

val e1 = Number 42; val e2 = Binary(e1, Div, Number 0); val e3 = Binary(Number 0, Gt, Number 1); val e4 = Cond(e3, e1, e2); val e5 = Cond(False, e2, e3); val add1 = Fn("x",Binary(Variable "x", Add, Number 1)); val e6 = Call(add1, Number 0); val e7 = Call(add1, True); val e8 = Lett("x", Number 5, Variable "x"); val badfact = Lett("fact", Fn("n", Cond(Binary(Variable "n", Eq, Number 1), Number 1, Binary(Variable "n", Mul, Call(Variable "fact", Binary(Variable "n", Sub, Number 1) ) ) )), Variable "fact"); val fact = Lettrec("fact", Fn("n", Cond(Binary(Variable "n", Eq, Number 1), Number 1, Binary(Variable "n", Mul, Call(Variable "fact", Binary(Variable "n", Sub, Number 1) ) ) )), Variable "fact"); val apply = Fn("x", Fn("f", Call(Variable "f", Variable "x"))); val sml_compose = fn f => fn g => fn x => f (g x); val compose = Lettrec("comp", Fn("f", Fn("g", Fn("x", Call(Variable "f", Call(Variable "g", Variable "x") )))), Variable "comp"); val sml_pair = fn x => fn y => fn z => z x y; val pair = Fn("x", Fn("y", Fn("z", Call(Call(Variable "z", Variable "x"), Variable "y" ) ))); val fst = Fn("x", Fn ("y", Variable "x")); val snd = Fn("x", Fn ("y", Variable "y")); (* The following is not typable in SML: val sml_dummy = let val pair = fn x => fn y => fn z => z x y in pair 5 end val sml_foo = sml_dummy true; *) val foo = Lett("dummy", Lett("pair", Fn("x", Fn("y", Fn("z", Call(Call(Variable "z", Variable "x"), Variable "y" ) ))), Call(Variable "pair", Number 5)), Call(Variable "dummy", True)); (* The following is not typable in SML: val rec sml_omega = (fn x => x x); *) val omega = Lettrec("om", Fn("x", Call(Variable "x", Variable "x")), Variable "om");

Results of type checking with my solution appear below. Note that the expressions *e5*, *e7*, *badfact*, and *omega* are rejected by the type checker:

- typecheck e1; val it = "int" : string - typecheck e2; val it = "int" : string - typecheck e3; val it = "bool" : string - typecheck e4; val it = "int" : string - typecheck e5; Types of conditional branches don't match true-clause: int false-clause: bool uncaught exception TypeError - typecheck add1; val it = "(int -> int)" : string - typecheck e6; val it = "int" : string - typecheck e7; Type of formal and actual parameters don't match uncaught exception TypeError - typecheck e8; val it = "int" : string - typecheck badfact; uncaught exception UnboundVar - typecheck fact; val it = "(int -> int)" : string - typecheck apply; val it = "(a -> ((a -> e) -> e))" : string - typecheck compose; val it = "((i -> j) -> ((d -> i) -> (d -> j)))" : string - typecheck pair; val it = "(a -> (b -> ((a -> (b -> i)) -> i)))" : string - typecheck fst; val it = "(a -> (b -> a))" : string - typecheck snd; val it = "(a -> (b -> b))" : string - typecheck foo; val it = "((int -> (bool -> i)) -> i)" : string - typecheck omega; uncaught exception CircularType