5 Type Checker
In this assignment, you will implement a static type checker for an extension of the Paret language, Typed Paret.
Chapter 15.1—15.2 of PLAI 2/e.
As in Interpreter
, we have provided a function parse
, which consumes an expression in Typed Paret’s concrete syntax and returns the abstract syntax representation (Expr
) of that expression.
You will implement one function called type-of:
that consumes a Paret program in abstract syntax form. If the program is well-typed, type-of returns the Type of that program; otherwise, it raises an exception.
Once you have implemented type-of
, you should use the provided type-check
function (analogous to eval
) to write test cases for your type checker in your testing file.
For simplicity, Typed Paret does not have syntactic sugar. let has been converted into a non-sugar expression (so type-of will handle let expressions directly), and and and or have been removed from the language.
5.4 Features to Implement
5.4.1 Type Environment
The type language you will work with is
(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.
Just as how Interpreter
had an Env
for mapping identifiers to values, your interpreter should use a type environment (TEnv
) to keep track of the types
of identifiers in scope.
(define-type-alias TEnv (Hashof Symbol Type))
In type-of, if the program binds an identifier that is already bound, the new binding should take precedence. This is known as identifier shadowing. The new binding shadows the existing binding.
Paret now contains support for lists via the constant empty and the operations link, is-empty, first, and rest. Lists in Paret are homogeneous: all elements in the list must have the same type.
A question to briefly consider: 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.
Thus, our typed list semantics are as follows:
(empty : t) makes an empty list whose elements have type t.
link :: t, (List t) -> (List t)
(link x y) prepends the element x to the list y.
first :: (List t) -> t
(first x) returns the first element of x.
rest :: (List t) -> (List t)
(rest x) returns the list x except for the first element of x.
is-empty :: (List t) -> Bool
(is-empty x) returns true if x is empty; otherwise, it returns false.
Whenever these type signatures are violated, the type checker should raise a tc-err-bad-arg-to-op exception.
Error-checking link should occur in the following manner: If the type of the second argument to link isn’t a (List t), the arg-type of tc-err-bad-arg-to-op should be the type of the second argument. If the second argument to link is a (List t) but the type of the first argument is not t, then the arg-type of tc-err-bad-arg-to-op should be the type of the first argument. For example,
(link "hello" 3)
(link 2 (empty : Bool))
should all raise (tc-err-bad-arg-to-op (op-link) (t-num)).
Most of the exceptions your type-checker can raise are just like the errors from Interpreter
, but with a type instead of a value.
There are two new kinds of exceptions, though:
tc-err-bad-arg-to-fun should be raised when a function is applied to an argument of the wrong type. func-type is the type of the function being applied, and arg-type is the type of the argument it was applied to.
tc-err-if-branches should be raised when an if statement has branches that have different types. then-type is the type of the “then” branch, and else-type is the type of the “else” branch. For instance,
should raise (tc-err-if-branches (t-num) (t-str)).
However, tc-err-if-got-non-boolean takes precedence over tc-err-if-branches. For example,
should raise (tc-err-if-got-non-boolean (t-str)) rather than (tc-err-if-branches (t-num) (t-str)).
Thus, the full set of exceptions is as follows:
(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]))
For tc-err-bad-arg-to-op, argument types to Operators should be checked from left to right. For example,
should raise (tc-err-bad-arg-to-op (op-plus) (t-bool)).
Finally, your type-checker should type-check by performing a post-order traversal of the AST: first, traverse all of the children of an expression from left to right, then check the expression itself. This makes it unambiguous which error to raise if there are multiple errors in the AST. For example,
(str= (+ 1 "bad") (++ 1 "bad"))
(++ false (+ "bad" 2))
("not function" (+ 3 "bad"))
(if true (+ 4 "bad") (++ 4 "bad"))
should all raise (tc-err-bad-arg-to-op (op-plus) (t-str)).
The grammar of Typed Paret is as follows:
<expr> ::= <num>
| (+ <expr> <expr>)
| (++ <expr> <expr>)
| (num= <expr> <expr>)
| (str= <expr> <expr>)
| (if <expr> <expr> <expr>)
| (<expr> <expr>)
| (lam (<id> : <type>) <expr>)
| (let (<id> <expr>) <expr>)
| (link <expr> <expr>)
| (first <expr>)
| (rest <expr>)
| (is-empty <expr>)
| (empty : <type>)
<type> ::= Num
| (List <type>)
| (<type> -> <type>)
Our parse function expects and enforces spaces around : and ->, so keep that in mind when you’re writing test cases.
5.5.1 Abstract Syntax
(e-num [x : Number])
(e-bool [x : Boolean])
(e-str [x : String])
(e-op [op : Operator]
[left : Expr]
[right : Expr])
(e-un-op [op : UnaryOperator]
[expr : Expr])
(e-if [cond : Expr]
[consq : Expr]
[altern : Expr])
(e-lam [param : Symbol]
[arg-type : Type]
[body : Expr])
(e-app [func : Expr]
[arg : Expr])
(e-id [name : Symbol])
(e-let [id : Symbol]
[value : Expr]
[body : Expr])
(e-empty [elem-type : Type]))
5.6 Testing Guidelines
For the purposes of testing, we have defined a type-check function that calls parse and type-of for you. type-check consumes an expression in Paret’s concrete syntax (S-Exp) and returns a Paret Type:
type-check :: S-Exp -> Type
You should use type-check in your testing file when writing test cases. You should not directly test type-of in your testing file.
In addition to the testing forms documented in the Testing Guidelines
, we provide the following testing form:
5.7 Starter Code
We’ve provided starter code for your implementation at type-checker.rkt
and support code at support.rkt
. You are not allowed to change the signature of type-check
, but you are welcome to add any helper functions that you need for your implementation.
We’ve also provided a stencil for your type-check
test cases at type-checker-tests.rkt
and testing support code at test-support.rkt
. You should check that you can run your type-checker-tests.rkt
file successfully in DrRacket before submitting—if you can’t, it means that a definition is missing or you’re trying to test a function that you shouldn’t be testing.
5.8 What To Hand In
You will submit two files for this assignment:
type-checker.rkt, which should be uploaded to the “Code” drop on Gradescope.
type-checker-tests.rkt, which should be uploaded to the “Tests” drop on Gradescope.
You can update your submissions as many times as you want before the deadline.