assignment 3

CPSC 521: Foundations of Functional Programming

Author: Robin Cockett

Due: End of Semester

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.

Your program (minimally) should allow you to determine whether a program is well-typed and display the program's most general type. In order to run a program, you should arrange that defined programs can be applied to inputs.