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

John H. E. Lasseter