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.
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.
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).
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.
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
- Examples from lecture XII (parsing combinators).
-
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.
This year's aren't yet available online, but should appear as Paper 12
Question 12 and Paper 13 Question 12.
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.
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.