Here is TLambda, a typed version of Lambda:
Lambda is one of:
Identifier
(lambda (TIdentifier ...) Lambda)
(let (TIdentifier Lambda) Lambda)
Number
(+ Lambda Lambda)
(if0 Lambda Lambda Lambda)
(letrec ((TIdentifier TIdentifier ...) Lambda) Lambda)
(set! Identifier Lambda)
(Lambda Lambda ...)
Identifier is a:
Symbol
TIdentifier is a:
(list Type Identifier)
Type is one of:
number
(Type ... -> Type)
Your first task is to make the interpreter for Lambda safe. That is, during evaluation, the interpreter must explicitly check that the values of all Lambda operations belong to the proper subset of values. Here is a tabular enumeration of restrictions:
| Identifier | no computation |
| (lambda (Identifier ...) Lambda) | no computation |
| (let (Identifier Lambda1) Lambda) | no restriction |
| Number | no computation |
| (+ Lambda1 Lambda2) | both Lambda1 and Lambda2 must evaluate to numbers |
| (if0 Lambda1 Lambda2 Lambda3) | Lambda1 must evaluate to a number |
| (letrec ((Identifier Identifier ...) Lambda) Lambda) | no restriction |
| (set! Identifier Lambda) | no restriction |
| (Lambda1 Lambda ...) | Lambda1 must evaluate to a closure |
Your second task is to modify the Lambda interpreter into a TLambda interpreter. The modified interpreter must parse the S-expression according to the new grammar and produce a modified ast; it must check the variable bindings on the modified ast; and it must check the types. If the type checker discovers errors, it must produce an ast with appropriate type error messages. The type checker may override syntactic information in the type checker to report a type error.
Suggestion: You do not need to produce error messages concerning the syntax of types. If types are syntactically incorrect, the parser may signal a general error for the corresponding binding construct.
The type checker implements the following proof system:
TEnv plus (t1 x1) ... |- e : t ------------------------------------------------ TEnv |- (lambda ((t1 x1) ...) e) : (t1 ... -> t) | TEnv |- e1 : (t1 ... -> t) TEnv |- e2 : t1 ... ---------------------- TEnv |- (e1 e2 ...) : t | |
TEnv contains (t x) ------------------- TEnv |- x : t | TEnv contains (t x) TEnv |- e : t ---------------------- TEnv |- (set! x e) : t | |
TEnv |- e1 : t1 TEnv plus (t1 x1) |- e : t -------------------------------------- TEnv |- (let ((t1 x1) e1) e) : t | TEnv plus ((t1 ... -> t) f) (t1 x1) ... |- e1 : t TEnv plus ((t1 ... -> t) f) |- e : t0 -------------------------------------------------- TEnv |- (letrec (((t f) (t1 x1) ...) e1) e) : t0 | |
------------------ TEnv |- n : number | TEnv |- e1 : number TEnv |- e2 : number -------------------------- TEnv |- (+ e1 e2) : number | TEnv |- e1 : number TEnv |- e2 : t TEnv |- e3 : t -------------------------- TEnv |- (if0 e1 e2 e3) : t |
| where t, t0, t1 are types and e1, e2, e3 are expressions. |
Since types do not play a role during evaluation, you must reuse the safe Lambda interpreter directly. (What do you have to do for that?) Furthermore, you must modify the safe interpreter so that it only performs those safety checks that the type checker cannot prove away. For example, if the safe interpreter contains the check
(unless (and (number? x) (number? y))
(error 'Lambda-interpret "safety check: ~s and ~s should be numbers" x y))
(Lambda-operation x y)
then the modified interpreter may contain
(unless (and (or type-check-done? (number? x)) (number? y))
(error 'Lambda-interpret "safety check: ~s and ~s should be numbers" x y))
(Lambda-operation x y)
where type-check-done? is a flag that is set to true
after the type checker has successfully checked the given program. In this
particular case, a successful type check would eliminate one of two safety
checks.
Your final task is to state a type safety theorem for TLambda.
The homework is due on Monday 13 November 2001 before class.
Expected size: 1,000 lines