Author: Robin Cockett

Date: 2nd December 2014

Due: 12th December midnight

Assignment #4: Type inference for BPCF.

The main requirement of this assignment is to develop a type inference algorithm for the simply typed lambda calculus with fixed points, pairs, natural numbers, and lists: I call this the Basic Programming language for Computable Functions (BPCF). To achieve this you will need to collect the type equations and to solve them incrementally. In addition, as an optional extra you can arrange for programs applied to values to be evaluated on the modern SECD machine.

This extension to the simply typed lambda calculus (BPCF): it is
described here together with the type
inference algorithm.

The deliverables for this assignment are:

- Input and output routines for BPCF programs and their types.
- An algorithm for collecting type equations and solving
them: this the main part of the assignment.

- Optional extra: an evaluator for BPCF programs using an
extended modern SECD machine. For this you must support
definitions of programs so that one can apply defined programs
to inputs.