CSCI 1730 · Fall 2026
3 Type Checker
3.1 Introduction
In this assignment, you will implement a static type checker for Typed Core Paret, and then, in a second stage, a desugarer for Typed Paret, so that the same sugar you added to the untyped language works in the typed one too.
3.2 Assignment
The assignment is in two stages, each with its own language and its own hand-in. In Stage 1: Type Checking you write a type checker, type_of, for Typed Core Paret. In Stage 2: Typed Desugaring you write a desugarer, desugar, from Typed Paret to Typed Core Paret, so that your checker, unchanged, checks the richer language too.
3.3 Stage 1: Type Checking
We have provided a module, tparet_core.rhm, that defines Typed Core Paret: its types Type, its abstract syntax Expr, and a parser
parse :: Sexp -> Expr |
parse_str :: String -> Expr |
You will implement one function:
type_of :: Expr -> Type |
which consumes the abstract syntax of a closed program. If the program is well-typed, type_of returns its Type; otherwise, it raises an error (see Errors). As with interp, type_of takes no environment: you will write a helper that does, and call it with the empty type environment.
3.3.1 Grammar
<expr> ::= <num> |
| <string> |
| <var> |
| true |
| false |
| (+ <expr> <expr>) |
| (++ <expr> <expr>) |
| (num= <expr> <expr>) |
| (str= <expr> <expr>) |
| (if <expr> <expr> <expr>) |
| (lam (<var> : <type>) <expr>) |
| (<expr> <expr>) |
|
<type> ::= Num |
| Str |
| Bool |
| (<type> -> <type>) |
The only difference from Core Paret is that a function’s parameter carries a type. Num, Str, and Bool are the types of numbers, strings, and Booleans, and (T1 -> T2) is the type of a (one-argument) function from T1 to T2.
3.3.2 Abstract Syntax
type Type |
| t_num() |
| t_str() |
| t_bool() |
| t_fun(arg :: Type, ret :: Type) |
|
type TEnv = Mapof(Symbol, Type) |
|
type Expr |
| e_num(n :: Int) |
| e_str(s :: String) |
| e_bool(b :: Boolean) |
| e_op(op :: Op, left :: Expr, right :: Expr) |
| e_if(cnd :: Expr, thn :: Expr, els :: Expr) |
| e_lam(param :: Symbol, param_type :: Type, body :: Expr) |
| e_app(fn :: Expr, arg :: Expr) |
| e_var(name :: Symbol) |
Op is as in the Interpreter. There are no values: a type checker never runs the program.
3.3.3 Features to Implement
3.3.3.1 Type Environment
Just as the Interpreter had an Env mapping variables to values, your type checker uses a type environment, TEnv, mapping variables to their types. It is a Mapof like Env, and shadowing works the same way: if the program binds a variable that is already bound, the new binding takes precedence. A variable that is not bound is a type error (see Errors).
3.3.3.2 Typing Rules
A number has type Num, a string Str, and true and false Bool.
+ requires both operands to have type Num and has type Num; ++ requires Str and has type Str; num= requires Num and has type Bool; str= requires Str and has type Bool.
if requires its condition to have type Bool and its two branches to have the same type, which is then the type of the whole expression. Unlike the interpreter, which evaluates only one branch, the checker checks both, whatever the condition is.
(lam (x : T) body) has type (T -> U), where U is the type of body in an environment where x has type T. The body is checked whether or not the function is ever applied.
An application (f a) requires f to have a function type (T -> U) and a to have exactly the type T, and then has type U.
Every requirement that is not met is a type error (see Errors). Wherever a rule says two types must be the same, it means exactly the same: two function types are the same only if their parameter types are the same and their return types are the same. (If you’re wondering what else it could possibly be, wait until we get to subtyping.)
3.3.3.3 Errors
Raise type errors with Shplait’s error, always with the symbol #’type_error, and a message that says what went wrong: e.g.,
error(#'type_error, "if: condition must be Bool, got " +& to_string(ct)) |
As in the Interpreter, Shplait converts the symbol to text at the front of the error message, so this error’s message begins with type_error:, and tests recognize a type error by matching the string "type_error" (see the Testing Guidelines).
3.3.4 Testing
Tests go in type_checker_tests.rhm, and every test goes through type_of applied to a parsed program:
check: |
type_of(parse_str("(+ 1 2)")) |
~is t_num() |
|
check: |
type_of(parse_str("(+ 1 \"a\")")) |
~raises "type_error" |
Types are ordinary values here, so unlike closures in the interpreter, you can and should test them for equality, function types included:
check: |
type_of(parse_str("(lam (x : Num) (+ x 1))")) |
~is t_fun(t_num(), t_num()) |
3.4 Stage 2: Typed Desugaring
Typed Paret adds to Typed Core Paret the sugar you already know from Desugar: and, or, and let. A second module, tparet.rhm, defines it: a Surface type and a parser
parse_surface :: Sexp -> Surface |
parse_surface_str :: String -> Surface |
(As in Desugar, these are named differently from tparet_core.rhm’s parse and parse_str, so that you can import both modules with open.)
You will implement one function:
desugar :: Surface -> Expr |
where Expr is the type from stage 1. A program’s type is then type_of(desugar(...)), using your stage 1 type checker unchanged: the sugar is handled entirely before the checker sees the program.
When we grade your desugar, we check the programs it produces with our type checker, which is correct. That way, a test fails only because of your desugar, never because of a bug in your type checker. Your stage 2 tests still use your own type checker, but you don’t hand it in again.
3.4.1 Grammar
<expr> ::= ... everything in Typed Core Paret ... |
| (and <expr> <expr>) |
| (or <expr> <expr>) |
| (let (<var> : <type> <expr>) <expr>) |
The meaning of the three forms is exactly as in Desugar: and and or short-circuit and are Boolean-strict, and let binds one variable, non-recursively. One thing has changed: the let of Typed Paret carries a type annotation for the variable it binds, which the untyped one did not. Start from your untyped desugarer and you will find out why.
3.4.2 Abstract Syntax
type Surface |
| s_num(n :: Int) |
| s_str(s :: String) |
| s_bool(b :: Boolean) |
| s_op(op :: Op, left :: Surface, right :: Surface) |
| s_if(cnd :: Surface, thn :: Surface, els :: Surface) |
| s_lam(param :: Symbol, param_type :: Type, body :: Surface) |
| s_app(fn :: Surface, arg :: Surface) |
| s_var(name :: Symbol) |
| s_and(left :: Surface, right :: Surface) |
| s_or(left :: Surface, right :: Surface) |
| s_let(name :: Symbol, name_type :: Type, rhs :: Surface, body :: Surface) |
Op, Type, and Expr are as in stage 1.
3.4.3 Testing
Tests go in typed_desugar_tests.rhm, and every test goes through the desugarer and then the checker:
check: |
type_of(desugar(parse_surface_str("(let (x : Num 1) (+ x 2))"))) |
~is t_num() |
The stencil imports both language modules and your two implementation modules, all with open; keep those imports as they are. Since the test file opens both of your modules, type_checker.rhm and typed_desugar.rhm must not define helper functions with the same name. As in Desugar, a test of the form desugar(...) ~is ... is invalid, since there is more than one correct desugaring.
Your stage 2 test file should be a superset of your stage 1 file: every Typed Core Paret program is a Typed Paret program. Then think about what the sugar does under a type checker. (and false 5) ran without error in the untyped language; what does the checker say about it, and why?
3.5 Starter Code
You are provided with:
type_checker.rhm, the stencil for your type checker.
type_checker_tests.rhm, the stencil for your stage 1 tests.
typed_desugar.rhm, the stencil for your desugarer.
typed_desugar_tests.rhm, the stencil for your stage 2 tests.
tparet_core.rhm and tparet.rhm, the two languages, with sexp.rhm and sexp.rkt, which they use to read S-expressions.
3.6 What To Hand In
Stage 1, to two Gradescope drops:
type_checker.rhm, to the “Code” drop.
type_checker_tests.rhm, to the “Tests” drop.
Stage 2, to two Gradescope drops:
typed_desugar.rhm, to the “Code” drop.
typed_desugar_tests.rhm, to the “Tests” drop.