# Project 3: Type checking

• Due: 03/08 at 11:55pm
• Points: 30

In this project, we’ll write a type checker for the simply-typed lambda calculus. It will take type-annotated lambda terms and check all the types; if the type check succeeds, it prints the result of evaluating the term, together with its type:

> let f = λx:Nat. succ (succ x) in f (f 0)
succ (succ (succ (succ 0))) : Nat

## 0. Getting started

The repository contains the following files (among others):

solution/
pcf.darwin  Reference implementation (MacOS)
pcf.linux   Reference implementation (Linux)
test/
test.sh     Test script
pcf.input   Test cases

Try running the reference implementation and have a look at the test cases to see how it works.

## 1. Syntax

To extend the syntax to include type annotations, we remove the rule

t ::= λx. t

and replace it with

t ::= λx:T. t

T ::= Nat
Bool
T -> T

The term λf:NatBool. f 0 would be represented as

["typedlambda", "f", ["arrow", "Nat", "Bool"], ["app", ["var", "f"], "zero"]]   (Python)
(typed-lambda "f" (arrow Nat Bool) (app (var "f") zero))                        (Scheme)
TypedLambda ("f", Arrow (Nat, Bool), App (Var "f", Zero))                       (OCaml)

## 2. Typechecking

Implement the type-checking rules from TAPL as a function that takes a typed λ-term t and returns the unique T such that t : T, or else raises an exception with an appropriate error message.

――――――――――               T-Var
Γ ⊢ x:Γ(x)

Γ, x:T1 ⊢ t2 : T2
――――――――――――――――――――――         T-Abs
Γ ⊢ λx:T1. t2 : T1T2

Γ ⊢ t1 : T2T   Γ ⊢ t2 : T2
――――――――――――――――――――――――――――     T-App
Γ ⊢ t1 t2 : T

―――――――――――              T-True
true : Bool

――――――――――――             T-False
false : Bool

t1 : Bool   t2 : T   t3 : T
―――――――――――――――――――――――――――      T-If
if t1 then t2 else t3 : T

―――――――                T-Zero
0 : Nat

t : Nat
――――――――――――              T-Succ
succ t : Nat

t : Nat
――――――――――――              T-Pred
pred t : Nat

t : Nat
―――――――――――――――             T-IsZero
iszero t : Bool

If you implemented fix as syntactic sugar, it’s important that you do desugaring after typechecking. So include the rules for both let and fix:

Γ ⊢ t1 : T1   Γ, x:T1 ⊢ t2 : T2
―――――――――――――――――――――――――――――――    T-Let
Γ ⊢ let x = t1 in t2 : T2

Γ ⊢ t1 : T1  T1
―――――――――――――――――           T-Fix
Γ ⊢ fix t1 : T1

## 3. Evaluation

You can integrate the typechecker into your PP2 interpreter in one of two ways:

• Implement a new function that converts a typed lambda term into an untyped term, simply by erasing the type annotations. Then the untyped term can be handed to the PP2 interpreter.

• Modify your PP2 interpreter to work directly on typed terms. (But there’s no need for the modified interpreter to actually do anything with the types.)

## 4. Read-eval-print loop

Your interpreter should be named submit/pcf. It should read lines from stdin, each containing exactly one term. For each term, it should evaluate the term and write a single line to stdout, which is either of the form v : T, where v is the result (with or without type annotations) and T is its type, or an error message that begins with the string error:. Run test/test.sh pcf to test your interpreter.

Please submit your code by pushing to your private repository and creating a tag pp3. If you’re submitting a single part, tag it pp3-2, pp3-3, etc.

Part Points
Booleans 6
numbers 8
λ-calculus 6
let 2
fix 2
evaluation 3
REPL 3
Total 30