7.3.4 C:   Type Checker
On this page: The Core Problem Desguaring The Language Exceptions Grammar Stencil Code Submission
7.3.4 C: Type Checker The Core Problem Desguaring The Language Exceptions Grammar Stencil Code Submission The Core Problem

In this assignment, you will define a function
type-of :: Expr -> Type
that implements a type-checker for Paret. If the program has a type, it computes it. If it does not, it raises an exception.

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. 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.

You will therefore need to write a modest desugarer to eliminate the syntactic sugar:
desugar :: Expr -> Expr
The expectation is that all syntactic sugars have been eliminated by desugar, so every program that consumes the output—such as an interpreter or type checker—does not need to know how to handle any of the eliminated constructs.

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! 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).

The type language you will work with is
(define-type Type
  (t-fun [arg-type : Type] [return-type : Type])
  (t-list [elem-type : Type]))
which, respectively, represent the types of numbers, Booleans, strings, (one-argument) functions, and (homogenous) lists.

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.

The list operations have the following types:
first :: (List t) -> t
rest :: (List t) -> (List t)
link :: t, (List t) -> (List t)
is-empty :: (List t) -> Bool
Whenever these types are violated, the type checker must signal an error.

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. Exceptions

The full set of exceptions is as follows:
(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]))
We hope these are self-explanatory.

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. 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>) Stencil Code Submission