CS 441 Assignment 7: Type Inference

This assignment is due thursday April 18 at 10:30am, by electronic submission.

Read the lecture notes for background. Feel free to work from my assignment 3 solution if you have trouble with yours.

Part 1

You are to build a static type inference algorithm for a language similar to that of assignment 3. Work from your meta-circular interpreter for part 1 of assignment 3. Support the following language:

 e ::= n                  
     | #t                 
     | #f                 
     | ()                 
     | (quote x)          
     | x
     | (if e e e)         
     | (begin e ...)         
     | (lambda (x ...) e) 
     | (let ((x e) ...) e)
     | (letrec ((x f) ...) e)
     | (e e ...)          
where n is a number, x is a variable, f is a lambda expression, and ... means zero or more of the previous item. Since part 1 of assignment 3 didn't have letrec, you'll have to add it, but you can do this easily by using letrec.

Your type grammar must include at least the following types, represented however you like:

 t ::= 'a              (type variable)
     | bool            (boolean)
     | num             (number)
     | sym             (symbol)
     | (t ... -> t)    (procedures of 0 or more arguments)
     | (t list)        (list of elements of type t)
Type variables are used mainly during the inference algorithm, but they may show up in the types of certain expressions, eg. (lambda (x) (car x)).

Support the following primitives:

 +, *, -, / : (num num -> num)
 =          : (num num -> bool)
 not        : (bool -> bool)
 symbol=    : (sym sym -> bool)
 cons       : ('a ('a list) -> ('a list))
 car        : (('a list) -> 'a)
 cdr        : (('a list) -> ('a list))
 pair?      : (('a list) -> bool)
 null?      : (('a list) -> bool)
 display    : ('a -> bool)
You may add to this set at your discretion. The display procedure displays a value of any type and returns #f.

Expressions should be typed according to the following typing rules.

    A |- n : num

    A |- #t : bool

    A |- #f : bool

    A |- () : (t list)

    A |- (quote x) : sym

     A(x) = t
    ----------
    A |- x : t

    A |- e1 : bool      A |- e2 : t      A |- e3 : t
    ------------------------------------------------
                A |- (if e1 e2 e3) : t

    A |- e1 : t1   ...   A |- en : tn
    ---------------------------------
       A |- (begin e1 ... en) : tn

          A[x1 -> t1]...[xn -> tn] |- e : t
    ----------------------------------------------
    A |- (lambda (x1 ... xn) e) : (t1 ... tn -> t)

    A |- e0 : (t1 ... tn -> t)      A |- ei : ti  (for i=1..n)
    ----------------------------------------------------------
                A |- (e0 e1 ... en) : t

    A |- ei : ti   (for i=1..n)     A[x1 -> t1]...[xn -> tn] |- e : t
    -----------------------------------------------------------------
                 A |- (let ((x1 e1) ... (xn en)) e) : t

    A[x1 -> t1]...[xn -> tn] |- ei : ti   (for i=1..n)
    A[x1 -> t1]...[xn -> tn] |- e : t
    --------------------------------------------------
        A |- (letrec ((x1 e1) ... (xn en)) e) : t
Note that the empty list, ie. (), has type (t list) for any element type t.

Part 2

Replace the typing rule for let expressions with the following rule:
    A |- ei : ti   (for i=1..n)     A |- e[x1 -> e1]...[xn -> en] : t
    -----------------------------------------------------------------
                 A |- (let ((x1 e1) ... (xn en)) e) : t
Now, a let expression is typed by checking that its bound expressions are typable, substituting the bindings throughout the body (avoiding capture by renaming bound variables!), and checking that the resulting expression is typable. Be sure that you use the expression arising from substitution only to compute the type of the let expression, not for evaluation.

Since only let expressions are polymorphic, in order to build a recursive procedure with a polymorphic type, you must do something like this:

(let ((last (letrec ((last (lambda (l)
                             (if (null? (cdr l))
                                 (car l)
                                 (last (cdr l))))))
              last)))
  (begin
    (display (last (cons 1 (cons 2 ()))))
    (display (last (cons 'x (cons 'y ()))))))

What to turn in

Turn in a single file that uses no load's other than cs441-load's and has no syntax errors. This file should define a function eval that takes an expression, parses it, type checks it using the Part 2 rule for let, and evaluates it only if it is type correct. Have the type checker print the type of the expression before evaluating it.