Introduction to Functional Programming

Andrew Gordon / adg@cl.cam.ac.uk

Computer Science Tripos, Part II (General) and Diploma in Computer Science. Twelve lectures. Lent 1995. Tu. Th. 12. Beginning Thursday 19 January. Heycock room.

Contents: syllabus, ML on CUS and PWF, advice on interacting with ML, examples, books, past exam questions, relevant Internet resources and research opportunities.

The objective of this course is to teach the central ideas of functional programming: list and symbolic processing, higher-order functions, lazy sequences, program specification and verification, type inference and programming with combinators. We will study one language, Standard ML, in depth, but I will also discuss the key ideas of lazy functional programming.

Larry Paulson developed the teaching materials I am using in this course. His book ML for the Working Programmer is recommended reading. A booklet, Introduction to Functional Programming, available from the bookshop, complements the textbook, and includes some material (principally on type inference) not covered there. Hardcopies of the slides are also available from the bookshop.

Here are textual and pictorial syntax diagrams for Standard ML, and a list of predefined identifiers. Remember that the structures and functors of Standard ML are not covered in this course.

Syllabus and Schedule

Beware: what follows is only a provisional schedule. I may vary the rate of lecturing.

1 Basics of Functional Programing (4 lectures)

Background: W W Gibbs. "Software's Chronic Crisis", Scientific American (September 1994).
P Hudak and M P Jones
"Haskell vs. Ada vs. C++ vs. Awk vs. ... An Experiment in Software Prototyping Productivity" Submitted to Journal of Functional Programming.
Chapters 2 and 3 of ML for the Working Programmer.

I Thursday 950119
Motivation. Imperative commands versus functional expressions. Evaluation strategies: call-by-value, call-by-name, call-by-need. Lazy evaluation.

II Tuesday 950124
Overview of Standard ML. Basic types: integers, reals, strings, Booleans. Structured types: tuples, lists, functions.

III Thursday 950126
Functions on lists: length, reverse, append. Recursion versus iteration. Utilities.

IV Tuesday 950131
Equality types. Sorting lists using quicksort and merge sort.

2 Datatypes (2 lectures)

Background: Chapter 4 of ML for the Working Programmer.

V Thursday 950202
Enumerated types. Pattern matching. Raising and handling exceptions. Binary trees; computing size and depth, traversing, balancing. Multi-branching trees, S-expressions.

VI Tuesday 950207
Binary search trees. Functional arrays. Propositional logic: negation normal form, conjunctive normal form.

3 Functions as First Class Citizens (2 lectures)

Background: J Hughes. "Why functional programming matters", Computer Journal 32:98-107 (1989).
Chapter 5 of ML for the Working Programmer.

VII Thursday 950209
Higher-order functions. Lambda-notation. Curried functions. Functionals: list summation, map, matrix multiplication, list folding.

VIII Tuesday 950214
Unbounded sequences. Consuming and joining sequences. Functionals on sequences. Numerical computations. Searching infinite trees.

4 Program specification and verification (2 lectures)

Background: Chapter 6 of ML for the Working Programmer.

IX Thursday 950216
Testing versus program verification. Formal versus rigorous proof. Proofs of ML programs. Mathematical and course-of-values induction.

X Tuesday 950221
Structural induction on lists. Proofs of appending and reversing. Structural induction on trees. Specification of sorting.

5 Further topics. (2 lectures)

Background: Section 8 of the Introduction to Functional Programming booklet, and the beginning of Chapter 9 of ML for the Working Programmer.

XI Thursday 950223
ML type inference. Polymorphism: types and type schemes. Axioms and inference rules.

XII Tuesday 950228
Case study: a functional parser. Parsing functionals: alternation, sequencing, transformation, repetition. Example: propositional logic.

ML on CUS and PWF

For the purposes of this course, ML is supported on CUS. CML, a local version of the Edinburgh ML compiler is available via the command /group/clteach/acn/ml/unix/cml. (An older version, without bignums, is also available at /home/mr10/edml/ml.) Please report any bugs to me (adg@cl.cam.ac.uk).

On the PWF machines, CML is present in the UTIL group. Just double-click on it to start. Please report any bugs to Arthur Norman (acn@cl.cam.ac.uk).

Advice on interacting with ML

Here's some advice on interacting with ML. Keep your ML code in a separate file, called fred.ML, say. Rather than type a long definition straight into ML, use an editor to add it to fred.ML. Run ML in a separate window, and cut and paste definitions from your editor window into your ML window. If ML complains that your code has a type error (which happens to me a lot), edit the definition in fred.ML, and then cut and paste it back into ML. This should save a lot of re-typing. Once you've built up several definitions, you can load them into ML by typing use "fred.ML";. This is useful at the beginning of a session, to get back to where you left off, or if you change a definition at the beginning of the file and want later definitions to take account of it.

Examples

There is a short example sheet to help get you started with ML.

Example programs from the course are available in directory /home/adg12/Intro-fp on CUS, or via the hypertext links below.

lists.ML
Examples from lectures III and IV (basic list processing and sorting).
datatypes.ML
Examples from lectures V and VI (user-defined datatypes).
functions.ML
Examples from lectures VII and VIII (higher-order functions).
parse.ML [New]
Examples from lecture XII (parsing combinators).

Books

L C Paulson.
ML for the Working Programmer (CUP, 1991) Good Buy!
Chris Reade
Elements of Functional Programming (Addison-Wesley, 1989)
A Wikström.
Functional Programming using ML (Prentice-Hall, 1987)
R S Bird and P Wadler.
Introduction to Functional Programming (Prentice-Hall, 1988)
R Harrison.
Abstract Datatypes in Standard ML (Wiley, 1993)
There are two books containing the formal definition of Standard ML, and a commentary.
R Milner, M Tofte and R Harper.
The Definition of Standard ML (MIT Press, 1990)
R Milner and M Tofte.
Commentary on Standard ML (MIT Press, 1991)
Beware: these last two are not textbooks, and make quite dense reading, but you may find them interesting to browse in a library.

Past Exam Questions

This year's aren't yet available online, but should appear as Paper 12 Question 12 and Paper 13 Question 12.

Internet Resources

For those interested, a good deal of information is available on the Internet about ML and functional languages generally. There is a general functional programming newsgroup, comp.lang.functional. I recommend you browse its associated FAQ (Frequently Asked Questions list) for a good overview of the various forms of functional languages and their implementations, and pointers to further Internet resources. Specific to ML, there is a newsgroup comp.lang.ml and an FAQ.

Research Opportunities

If you like functional programming, you may be interested in pursuing the subject towards a PhD. Research at the Lab focusses both on applications and theory of functional programming. The Automated Reasoning group develops and applies the HOL and Isabelle theorem-proving systems. These are amongst the largest applications developed using ML and have substantial communities of users outwith the Lab. In the area of Theory and Semantics, there is active research on semantics of Standard ML and on functional languages generally. Speak to me or any of the other lecturers if you are interested.