Foundations of Functional Programming

Lecturer: Dr A.C. Norman

No. of lectures: 12

This course is a prerequisite for Types (Part II).

Aims

• To show how lambda-calculus and related theories can provide a foundation for a large part of practical programming.

• To present students with one particular type analysis algorithms so that they will be better able to appreciate the Part II Types course.

• To provide a bridge between the Part IA Foundations of Computer Science course and the theory options in Part II.

Part A. The theory

• Introduction. Combinators. Constants and Free Variables. Reduction. Equality. the Church-Rosser theorem. Normal forms.

• The Lambda calculus. Lambda-terms, alpha and beta conversions. Free and bound variables. Abbreviations in the notation. Pure and applied lambda calculi. Relationship between combinators, lambda calculus and typical programming languages.

• Encoding of data: booleans, tuples, lists and trees, numbers. The treatment of recursion: the Y combinator and its use.

• Modelling imperative programming styles: handling state information and the continuation-passing style.

• Relationship between this and Turing computability, the halting problem etc.

Part B. Implementation techniques

• Combinator reduction as tree-rewrites. Conversion from lambda-calculus to combinators. The treatment of lambda-bindings in an interpreter: the environment. Closures. ML implementation of lambda-calculus. SECD machine. Brief survey of performance issues.

Part C. Type reconstruction

• Let-polymorphism reviewed following the Part IA coverage of ML. Unification. A type-reconstruction algorithm. Decidability and potential costs.

Objectives

At the end of the course students should

• understand the rules for the construction and processing of terms in the lambda calculus and of Combinators

• know how to model all major aspects of general-purpose computation in terms of these primitives

• be able to derive ML-style type judgements for languages based upon the lambda-calculus

Recommended books

Hindley, J.R. & Seldin, J.P. (1986). Introduction to combinators and lambda-calculus. Cambridge University Press (now out of print but try a library).
Revesz, G.E. (1988). Lambda calculus, combinators and functional programming. Cambridge University Press (now out of print but try a library).