McMaster University
CAS 706

Assignment 3

Typed Lambda-calculus interpreter.

Your term language should be based on the same term language as A2. The operational semantics is the same as for A2, and the same as in the textbook.

You should first write down the typing rules for your language. You are allowed, even highly encouraged, to improve the A2 grammar to make your life easier, so that typing rules can be made simpler. Your task is to have your interpreter first do type reconstruction for all inputs before any reduction is done. Decent error messages should be returned for untypable terms. The interpreter should then proceed as in assignment 2.

You should also be providing some test cases for your interpreter - make sure to test higher-order functions as well as cases that do not type (such as old stuck cases from assignment 2) and cases that work but are rejected in your typed language.

You should try to leverage the host system as much as you can for this assignment. This can mean having the type inference algorithm return a typed term, from a different ADT, than the original source. Then your interpreter can be much much simpler (and it should be) because all the 'impossible' cases have been removed already.

In other words, you are writing a type inference routine as the most important part of this assignment. The unification algorithm is thus key.

Bonus: implement an interpreter for your language but using the finally tagless method (in whatever language you want, but this is easiest in Haskell/Scala/Ocaml; more bonus for more languages. Can even be done in Agda/Idris). Note that this is cheating, in the sense that even though it is typed, the types are maintained by the host language, so that there is no need to implement unification (or even a separate typing pass) at all!

Nov. 2017