#lang racket #| CSC 324 2017 Fall Assignment 3 |# #| A Type Checker with some Inference |# (provide type) ; Implement ‘type’. #| The Language of Types. Base types: Boolean, Number, String, Void, and ⊥ [called “bottom”, \bot]. • Represented by symbols with those names. Function type constructor: ( ... → ) • Represented by a list of zero or more types, followed by the symbol →, followed by a type. |# #| The Syntactic Language of Expressions. - represented by a boolean, number, or string. - represented by a symbol. For each of the following, a list with that structure, where ‘...’ means zero or more of the preceding component, parts in angle-brackets are from the corresponding category, and other non-list components appear literally as symbols. Except: is never ⊥. (λ (( : ) ...) ... ) (let ([ ] ...) ... ) (rec ( ( : ) ... : ) ... ) ( ...) (if ) (set! ) |# #| The Type of an Expression. As with evaluation, the type of an expression is relative to a current environment that contains a mapping of variables in scope to their types. Also, if at any point a type during the check of an expression is ⊥, the type of the whole expression is ⊥, and the expression is said to “not type check”. : the corresponding base type : the type of the most local identifier with that name in the environment (λ (( : ) ...) ... ) • In the current environment with each bound locally to its corresponding : if each type checks then the type is ( ... → ), where is the type of . (let ([ ] ...) ... ) • If ... type check as ..., then the type is the same as the type of: ((λ (( : ) ...) ... ) ...) (rec ( ( : ) ... : ) ... ) • In the current environment with bound locally to , the type is the same as the type of: (λ (( : ) ...) ... ) ( ...) • Type checks iff the type of is a function type and the types of ... match the function type's argument types, in which case the type is the function type's result type. (if ) • Type checks iff the type of the condition is Boolean, and the consequent and alternative have the same type, in which case the type of the expression is the type of the consequent. (set! ) • Type checks iff the type of the most local identifier with that name in the environment is the type of , in which case the type is Void. |# ; type : Expression → Type ; You may choose whatever representation for the environment that you like. (define (type expr [env '()]) '⊥)