7.3.4 C: Type Checker
7.3.4.1 The Core Problem
type-of :: Expr -> Type
Your type checker will need a type environment just as your C: Interpreter needed a value environment. This is defined by the type TEnv, below.
7.3.4.2 Desguaring
We have extended Paret from C: Interpreter with some syntactic sugar to make it easier to program in the language. Concretely, we have added the constructs and, or, and (non-recursive) let. In principle, all three can be handled by the type checker, but then they would also need to be handled by the interpreter and all other tools. Instead, we will desugar them, i.e., rewrite them into terms in a smaller language.
desugar :: Expr -> Expr
One comment, to avoid confusion: Racket macros are themselves syntactic sugar. However, we are not asking you to use Racket macros for anything. Rather, you are going to build a tiny macro expander of your own, which will give you a soupçon of taste of how the Racket macro expander itself works.
There are multiple implementation strategies possible. You do not need to write a generic desugarer; it’s sufficient to write a desugar function that handles just those three constructs. Be sure to test it well: it’s easy to miss some details when desugaring!
7.3.4.3 The Language
We have also enriched the Paret language from C: Interpreter with lists: the constant empty and the operations link, is-empty, first, and rest. In addition, function definitions now require the type of the argument to be explicitly annotated (in A: Type Inference we will see how to lift this).
(define-type Type (t-num) (t-bool) (t-str) (t-fun [arg-type : Type] [return-type : Type]) (t-list [elem-type : Type]))
This language poses an interesting question: What is the type of the empty list? It’s polymorphic: it can be a list of any type at all! Because it has no elements, there’s nothing to constrain its type. However, because our type checker is not polymorphic, we handle this with a simple expedient: we require that every empty list be annotated with a type for the elements (that will eventually be linked to it). Naturally, the elements that eventually are linked to it must be consistent with that annotated type.
first :: (List t) -> t rest :: (List t) -> (List t) link :: t, (List t) -> (List t) is-empty :: (List t) -> Bool
The types of the remaining constructs are straightforward. In a conditional, the cond must be of type Bool, and the two branches must have the same type. It would be instructive to compare this to what happens in languages like B: TypeScript.
7.3.4.4 Exceptions
(define-type TypeCheckingError (tc-err-if-got-non-boolean [cond-type : Type]) (tc-err-bad-arg-to-op [op : Operator] [arg-type : Type]) (tc-err-bad-arg-to-un-op [op : UnaryOperator] [arg-type : Type]) (tc-err-unbound-id [name : Symbol]) (tc-err-not-a-function [func-type : Type]) (tc-err-bad-arg-to-fun [func-type : Type] [arg-type : Type]) (tc-err-if-branches [then-type : Type] [else-type : Type]))
You should type-check in the following order: first check the children of an expression from left to right, then check the expression itself (i.e., perform a post-order traversal of the tree). This makes unambiguous which error to raise if there are multiple errors.
7.3.4.5 Grammar
Remember to put spaces around : and -> because the parser expects them.
<expr> ::= <num> |
| <str> |
| <id> |
| true | false |
| (+ <expr> <expr>) |
| (++ <expr> <expr>) |
| (num= <expr> <expr>) |
| (str= <expr> <expr>) |
| (link <expr> <expr>) |
| (if <expr> <expr> <expr>) |
| (lam (<id> : <type>) <expr>) |
| (let (<id> <expr> : <type>) <expr>) |
| (<expr> <expr>) |
| (first <expr>) |
| (rest <expr>) |
| (is-empty <expr>) |
| (empty : <type>) |
|
<type> ::= Num |
| Str |
| Bool |
| (List <type>) |
| (<type> -> <type>) |