CSE 340 Homework 7

Due: Friday, April 16th. EXTENDED to Monday April 19th!
What to turn in: Two version of typeUnify.ml. The first should contain the modifications for part 1 and the second should start with your answer for part 1 and include the modifications for part 2.

In this assignment, you will have to work on an implementation of a type inferencer found here.  To compile this program the first time, you will need to do the following:

touch .depend
make depend
make               (ignore the error message)
make depend
make

The language for this assignment is almost the same as that for homework 5. However in this language, any type annotation may be replaced with a "?".

<primitive> ::= + | * | - | zero? | cons | hd | tl |  null? | pair | fst | snd 

<expr> ::= <number>     
    | <id>                  
    | false | true      
    | []   // empty list does not need its type    
    | <primitive> (<expr>*(,))  
    | proc ( {<annot> <id>}*(,)) <expr> 
    | (<expr>  <expr>)    
    | let <id> = <expr> in <expr>
    | letrec { <annot> <id> (<annot> <id>*(,))= <expr> }+ in <expr>                                
    | if <expr> then <expr> else <expr>  
    | set <id> = <expr>
    | begin <expr>+(;) end
    
<annot> ::= <type> | ?

<type> ::= int
   | bool 
   | (<type>*(*) -> <type>) // type of functions 
   | (<type> * <type>)      // type of pairs 
   | list (<type>)          // type of lists   

1. Finish the implementation of the unification-based type checker in the file typeUnify.ml, replacing all of the "raise TODO" lines with appropriate code. There are a two differences between this checker and the one that we described in class. The first is that type annotations are references to type options, so that after we determine the substitutions for the type variables, we can crawl over the expression and replace each "?" with the appropriate type. The second big difference is that this checker calls unify with each recursive call to type_exp. That way, we can give better error messages when the types do not match---we'll know exactly what expression we were checking where the error occurred.
    
2. Add let-polymorphism to this calculus, based on the description given in class on Wednesday, April 7.
   1. Change type environments to map variables to type schemes.

      type typ_scheme = Mono of typ | Poly of var list * typ
      type tenv = typ_scheme Env.env
      

   2. Modify the case for type checking let to generalize the types of the right-hand-sides before sticking them into the environment. Note that it is only safe to generalize when the right-hand-side of a let expression is a syntactic value.  Use the following definition for values:

      <value> ::= <number> | false | true | [] | proc ( {<annot> <id>}*(,)) <expr>
      

   3. Modify the case for variables to deal with polymorphic types in the type environment. When a Poly is found, the listed variables must be instantiated---replaced with fresh variables in the polymorphic type.
       
   4. Test your code on several polymorphic functions. Put some of your test cases in comments in your file.
       
   5. (Extra credit) Modify the case for type checking letrec to generalize the types of recursive functions before adding them to the environment that checks the body of the letrec. In this case, we do not have to worry about the value restriction because the right-hand-side of these definitions will always be functions.