Computer Laboratory – Course material 2007–08: Foundations of Functional Programming

Next: Mathematical Methods for Computer Up: Lent Term 2008: Part Previous: Digital Communication I Contents

Foundations of Functional Programming

Lecturer: Dr M.J. Parkinson

No. of lectures: 12

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

Aims

This course aims (a) to show how lambda-calculus and related theories can provide a foundation for a large part of practical programming, (b) to present students with one particular type analysis algorithm so that they will be better able to appreciate the Part II Types course, and (c) to provide a bridge between the Part IA Foundations of Computer Science course and the theory options in Part II.

Lectures

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. Eager and Lazy evaluation.
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. Return address seen as an additional continuation parameter.
Relationship between this and Turing computability, the halting problem etc.
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.
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 combinatory terms and terms in the lambda calculus
know how to model all major aspects of general-purpose computation in terms of these primitives
know how lambda terms may be efficiently interpreted by machine
be able to derive ML-style type judgements for languages based upon the lambda-calculus

Recommended reading

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).

Next: Mathematical Methods for Computer Up: Lent Term 2008: Part Previous: Digital Communication I Contents