CMSC 22610, Winter 2011
Homework 6, Due Thursday, Feb 24, 2011

Notation. In this file we are using purely ascii notation.  It should be viewed with a fixed-width font.

  * polymorphic type variables:  lower-case alphanumeric, e.g. a,b,c
  * polymorphic types:  fst: [a,b].a * b -> a,   Cons: [a].a * List a -> List a
  * unification variables:  U,V,W,X,Y,Z, with primes or "subscripts", e.g. X', X3
  * Clos(VE,ty) : relative closure of type expression ty wrt value environment VE
  * (R-13) : reference to typing rule (13) of the Project 3 description.
  * FunDec, finbind etc.: constructors or types defined in the Syntax module.

Example: Type checking the declaration "fun f x = let fun g y = (x,y) in g 3 end".

01  VE0                   fun f x = let fun g y = (x,y) in g 3 end  =>  VE0, f : Clos(VE0,X0)       FunDec  (R-15)
02                          f x = let fun g y = (x,y) in g 3 end    =>  X1 -> X2                    funbind (R-16)      X0 = X1 -> X2
03                            x                                     =>  (x:X3, X3)	            VarPat  (R-32)      X1 = X3
04  V1=VE0,x:X3               let fun g y = (x,y) in g 3 end        =>  X4                          LetExp  (R-17)
05                              fun g y = (x,y)                     =>  VE1, g : Clos(VE1,X5)       FunDec  (R-15)
06                                g y = (x,y)                       =>  X6 -> X7                    funbind (R-16)      X5 = X6 -> X7
07                                  y                               =>  (y:X8, X8)                  VarPat  (R-32)      X6 = X8
08  V2=VE1,y:X8                     (x,y)                           =>  X9 * X10                    TupleExp(R-23)      X7 = X9 * X10
09                                    x                             =>  X3                          VarExp  (R-25)      X9 = X3
10                                    y                             =>  X8                          VarExp  (R-25)      X10 = X8
11                                                                                                  Unify               X5 = X8 -> X3 * X8 
12  
13  VE1,g: [a].a->X3* a         g 3                                 =>  X11                         AppExp  (R-20)
14                                g                                 =>  X12->X3*X12                 VarExp  (R-25)      X11 = X3*X12
15                                3                                 =>  Int                         IntExp  (R-26)
16  
17                                                                                                  Unify               X11 = X3*Int
18                                                                                                  Unify               X4 = X3*Int
19                                                                                                  Unify               X2 = X3*Int
20                                                                                                  Unify               X0 = X3->X3*Int
21  => VE0, f: [a].a->a*Int  == Clos(VE0, X3->X3*Int)

This development of a typing for the example function declaration is very similar to the process of Algorithm W, though
algorithm W introduces fewer unification variables (e.g. X4, X5, X6, X7, X11 would not be introduced by Algorithm W).


Exercise 1: Show what would happen if at lines 05/13 the closure (i.e. generalization) of the type of g ignored the
fact that X3 occurs free in VE1 and generalized X3 as well as X8.


Exercise 2: Redo this development for the declaration 

   fun f x = let fun g y = Cons(y,x) in g 3 end

under the assumption that EV0(Cons) = [a].a * List a -> List a.


Exercise 3: Give a typing derivation similar to the above example for the following declaration:

   fun f (u,v) =
       let val x = u
           fun g z = Cons(z,x)
        in g (Cons(v,Nil))
       end

(where we assume EV0(Nil) = [a].List a).