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
submit/       Please place your code here

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:Nat→Bool. 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 : T1→T2            
                                  
  Γ ⊢ t1 : T2→T   Γ ⊢ 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.

Rubric

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