3.3 Problem: Types
Design a reduction system that models type checking by
reducing terms to their types. Formulate a metafunction that maps terms to
types or #false:
(define-metafunction TLambda-tc tc : e -> t or #false ; more here .....)
It produces #false when type checking fails.
You start with the normal term language:
(define-language TLambda (e ::= n x (lambda (x t) e) (e e) (+ e e)) (n ::= number) (t ::= int (t -> t)) (x ::= variable-not-otherwise-mentioned))
The reduction systems gradually reduces terms to types, like this:
(define type-checking (reduction-relation (--> (in-hole C n) (in-hole C int)) (--> (in-hole C (+ int int)) (in-hole C int)) ; you need more here .....))
Hint The key is to design a language of contexts that extends the given expression language so the reduction system can find all possible terms.
Consider adding if and let expressions to the language once you have the core model working.