CSE 340 HW 5

Due Date: March 29th, 2004
What to submit: An archive named by your last name (in tar or zip format) containing tests.tpl and typecheck.ml. 

Part I

In the type-checked language from lecture, the types for function arguments and letrec-function results must be declared explicitly by the programmer.

Convert the following to well-typed expressions by replacing ? with a suitable type expression. In all cases, use the shortest type expression possible. For example, given the first near-expression (proc(? x)x), convert it to (proc (int x) x), as opposed to proc((int -> int)x) x. Note: consider the type int to be shorter than the type bool.

proc (? x) x

let f = proc (? x) x 
 in (f 10)

let f = proc (? x)  x 
    g = proc (? y) y
   in (g f)

let f = proc (? x) x
    g = proc (? y) (y false)
in 
   (g f)

let f = proc (? x, ? z) x 
    g = proc (? y)  (y false 10)
in
   (g f)

let f = proc (? x) proc(? z) x 
    g = proc (? y)  ((y false) 10)
in
   (g f)

letrec ? f (? x) = x 
   in (f false)

letrec ? f (? x) = (f x)
   in (f false)

letrec ? f (? x, ? w) = (f x w)
   in (f false 12)

Put your answers in a file named tests.tpl and use that file to test the second part of your assignment.

Part II

Your task is to finish the implementation of a type checker for a call-by-value language extended with a simple type system. The archive hw5.tar provides a starting point for this implementation, including a complete interpreter, starting point, including a complete interpreter, datatype definitions for types, and some of the implementation of a type checker in the file typecheck.ml. The three parts of this problem ask you to extend the type checker in typecheck.ml.

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

<expr> ::= <number>
| <id> | false | true | []:<type> // empty list must be marked with its type | <primitive> (<expr>*(,))
| proc ( {<type> <id>}*(,)) <expr> | (<expr> <expr>)
| let <id> = <expr> in <expr> | letrec { <typ> <id> (<type> <id>*(,))= <expr> }+ in <expr>
| if <expr> then <expr> else <expr> | set <id> = <expr> | begin <expr>+(;) end

The type system includes the number type, boolean type, function types, list types and pair types:

 <type> ::= num
| bool
| (<type>*(*) -> <type>) // type of functions
| (<type> * <type>) // type of pairs | list (<type>) // type of lists
  1. Finish the type checker for if, variable assignment, letrec and let according to the rules discussed in class. Also add five tests (in comments) to the end of tests.tpl that cause type errors for these expression forms.
  2. Finish the type checker for products and add three programs to tests.tpl that use products that type check and three programs that do not type check. In the type checker, add the cases in check_prim for pair fst and snd according to the following rules:
    	E |- e1 : t1     E |- e2 : t2
    	-----------------------------
    	E |- pair(e1,e2) : (t1 * t2)
    	
    	E |- e : (t1 * t2)
    	------------------
    	E |- fst e : t1
    	
    
    	E |- e : (t1 * t2)
    	------------------
    	E |- snd e : t2 
    	
     
  3. Finish the typechecker for lists and add three programs to tests.tpl that use lists that type check and three programs that do not type check. This means adding the cases in check_prim for cons, hd, tl, and null? as well as the case in type_exp for null. You should use the following rules for guidance:
    E |- []:list(t)  : list(t)

    E |- e : list(t)
    ---------------
    E |- null?(e) : bool

    E |- e1 : t1 E |- e2 : list(t1)
    ------------------------------
    E |- cons(e1, e2) : list(t1)

    E |- e1 : list(t1)
    -------------------
    E |- hd(e1) : t1

    E |- e1 : list(t1)
    -------------------
    E |- tl(e1) : list(t1)