Functional Programming and Specification: Summary

Functional Programming and Specification: Summary

General

The lecture log indicates which topics were covered when, and the examples log contains all of the examples I used in the lectures. Last year's exam paper can be found on the course web page. Exam papers from earlier years are only partly relevant because the exam now covers only the first two parts of the course rather than the entire course, and because these were not on-line exams.

ML core language

Topics covered: Motivation. Values and their types, functions as ordinary values. Built-in types, type constructors, values and functions. Basic expressions. Function and value type bindings. Pattern matching, local declarations, recursive and mutually recursive function definitions, proof by induction. List processing, tree-like data structures. Static (lexical) scoping, higher-order functions, curried and non-curried functions. Lazy and eager evaluation. Strong typing, static typing, type inference, polymorphism, principal types, equality types. Type bindings, datatype definitions and value constructors, recursive and mutually recursive datatype definitions, structural induction. Exceptions, references and character input/output.

Reading: In this part of the course I followed chapters 2-14 of Harper's book fairly closely although I omitted a few topics, stressed some topics more or less than he did and used variants of one or two of his examples. I covered the material in his chapter 15 in quite a different way; see Lecture Note 1. A topic that is missing from Harper's book (equality types) is covered on the last half-page of that note. Essentially the same material is covered in almost any book or tutorial on ML including Paulson's book (chapters 1-5 and 8, minus the stuff about structures and signatures) and Gilmore's tutorial (all except the last chapter), and reading any one of these would usefully complement the presentation in the lectures. Another source is chapters 1, 2 and 4 of the precursor to Harper's book, This covers a dialect of ML that is now obsolete, but the differences are very minor. It is nice and short and so still worth reading as a summary of the main important ideas in ML. Another short summary, written by a previous FPS student, is here. (Disclaimer: I have not read this in detail! If it contains errors or misleading information then that is your problem.)

Revising: Read your tutor's comments on your solution to Practical 1. Use these comments to improve your solution. After doing this, compare the sample solution to Practical 1 with your solution. Do some exercises from Paulson's book.

What you are expected to know: The stress is on the underlying concepts and the way that one expresses algorithms and represents data in a functional language. You will be expected to produce working programs, but you will have the ML compiler and typechecker to help you. I expect you to be able to make reasonable use of the features of the ML core language. The Moscow ML library and its documentation will be available.

ML modules

Topics covered: Motivation and overview. Analogy between values, types and functions in the core language and structures, signatures and functors in the module language. Signatures as specifications of program units, signature inheritance. Structures as program units, qualified names. Signature matching and signature ascription, transparent versus opaque ascription, data abstraction. Module hierarchies, substructures; shared components, sharing specifications for avoiding confusion between different versions. Functors as parametrised structures; sharing specifications in functor parameter lists for ensuring compatibility.

Reading: In this part of the course I followed chapters 18-23 of Harper's book. This material is not covered well in some books and tutorials on ML; in particular, the coverage of modules in the last chapter of Gilmore's notes is not extensive enough for the purposes of this course. Alternative presentations of the material are in Paulson's book (the stuff about structures and signatures in chapters 2-5, plus chapter 7) and Tofte's lecture notes. Another source is chapter 3 of the precursor to Harper's book. The chapters of Harper's book that cover modules contain more errors than the earlier chapters and the explanation is lacking in places. Since many people find this material a little difficult, I recommend that you consult one of these other sources as well.

Revising: Read your tutor's comments on your solution to Practical 2. Use these comments to improve your solution. After doing this, compare the sample solution to Practical 2 with your solution. Do some exercises from Paulson's book and/or the exercise in part 2 of Tofte's lecture notes.

What you are expected to know: Again, the stress is on concepts. I expect you to be able to make reasonable use of the ML module facilities to organize ML programs, and to understand the issues involved in modular design. Examination questions involving modules generally do not involving writing a lot of code; you would not normally be asked to design a module structure and write code from scratch to go in the modules. You will have the ML compiler and typechecker to help you sort out sharing problems etc.

Specifying and developing ML programs in Extended ML

This part of the course is assessed by Practical 3 and is not covered in the examination!

Topics covered: Motivation. EML as a wide-spectrum language. Specifications. Using first-order equational axioms to specify ML functions. Loose specifications. Proving that a function satisfies a specification. Deriving structural induction principles from datatype declarations. Specifying structures and functors using signatures containing axioms. Proving that a structure/functor satisfies a specification. ML "computational" equality (=) versus EML "logical" equality (==).

Reading: Most of what you need to know about the material in this part of the course is in the following lecture notes:

These notes are derived from the sequence of examples in my paper "Formal specification of ML programs" which contains more detailed explanations but the lecture notes use more up-to-date notation and fix some errors. For background, it might be useful to read the presentation of formal development of ML programs in EML in section 4 of my paper "Formal program development in Extended ML for the working programmer". In all of these, attention is restricted to total functions that return non-exceptional values. Some other papers on EML do not make this restriction.

Revising: Read your tutor's comments on your solution to Practical 3. Use these comments to improve your solution. After doing all this, compare the sample solution to Practical 3 with your solution. Read VanInwegen's notes on how to write proofs. Practice doing proofs by induction, using the examples covered in lectures. Try specifying some basic functions and data structures like the ones in the Moscow ML library.

What you are expected to know: I expect you to be able to use EML to specify ML programs (involving only total functions returning non-exceptional values) and to verify the correctness of programs with respect to such specifications. The precise syntax of axioms in EML is not important, but axioms must be understandable as formal assertions in first-order logic. In specifying programs, concentrate on giving properties that the program must satisfy and forget about how the specified behaviour will be implemented unless you are asked for an implementation. In proofs, concentrate first on stating clearly what it is you are trying to prove. Proving properties of recursive programs will usually require the use of structural induction with respect to the argument type. In induction proofs, the most important thing is to be clear in the "step" case about what the induction hypothesis is and what it is that you are trying to prove using this hypothesis. The second most important thing is to make it clear where in the proof you make use of this hypothesis.


Don Sannella. Please mail me if you have any comments on this page.
Last modified: Sat Apr 30 12:58:11 BST 2011