Read the lecture notes for background. Feel free to work from my assignment 3 solution if you have trouble with yours.
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) : tNote that the empty list, ie.
()
, has type
(t list)
for any element type t
.
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) : tNow, 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 ()))))))
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.