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.
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.
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
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
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)