Functional Programming and Specification

I guess I like to have fun. - Madonna

These things are fun, and fun is good. - Dr Seuss

Most of the time I don't have much fun. The rest of the time I don't have any fun at all. - Woody Allen

Time, place, scope

This course runs in semester 2. Lectures take place in David Hume Tower, room 4.18, at 1110-1200 on Tuesday and Friday.

The tutorials are at 1400-1450 on Tuesday and Friday. If you want to change tutorial group then please ask the ITO to change it, not me.

Here is a detailed summary of what I covered and what I expect students to have learned, with ideas for revision.

Lecture log and examples

The lecture log is a concise record of the lectures on the course, with pointers to the corresponding reading.

These examples from the lectures are suitable for cutting and pasting into an SML or EML session. (Don't forget that you need to type a semicolon to indicate that you are finished before SML/EML will spring into action!)

Exercises

There will be three practical exercises. The first two exercises will be marked but the mark will not contribute to the overall mark for the course. It is in your interest to attempt them and submit them anyway - last year there was a very strong correlation between submission of these exercise and passing marks in the examination. The third exercise will contribute 20% of the overall mark for the course.

• Practical 1 was issued on Fri 14 Jan, and was due at 4pm on Tue 8 Feb. Here is a sample solution.
• Practical 2 was issued on Tue 8 Feb, and is due at 4pm on Tue 8 Mar. It is an exercise in modularising this ML program. Here is a sample solution.
  I suggest that you work on this exercise in pairs. Here is the Moscow ML Owner's Manual, mentioned under "If you want to learn more". You may find it helpful to look at the sample solution to the 2009 version of Practical 2. (The original unmodular version is here.)
• Practical 3 was issued on Tuesday 8 March and is due at 4pm on on Monday 21 March. It is an exercise in specification and proof. It will be marked and the mark will contribute 20% of the overall mark for the course. Here is a sample solution.

Here is some useful advice for how to go about attacking exercises like the ones in this course.

If you need an extension for coursework for some good reason, then:

• UG3 students: Please use this form.
• MSc students: Please email the Course Organiser.

I am not supposed to grant extensions, and neither is your tutor, so there is no point in asking us.

Moscow ML documentation

The Moscow ML library manual (2-up postscript version).

Here is a handy excerpt from the Moscow ML Language Overview listing all the built-in functions, which library modules are preloaded by default, etc.

For interactive documentation, try typing

help "topic";

in Moscow ML for information about topic.

There are various manuals at the Moscow ML website.

Running Standard ML

On Linux

Type mosml to the shell to start Moscow ML version 2.01. Then type use "file.sml"; to load an SML source file called file.sml. Type control-D to quit.

In lectures I run Moscow ML within xemacs which is convenient for cutting and pasting text in a session. When I run Moscow ML outside lectures I use a line editor called ledit (from here) which allows you to edit your previous input. To use it in DICE: download this file and put it in ~/ledit, make it executable by issuing the command

chmod 755 ~/ledit

and then put the following in ~/.brc:

alias mosml='~/ledit -h ~/.ml_history -x mosml'

And then take the Computer Security course to understand why you should never do what you have just done.

If you have a home machine

Moscow ML version 2.01 is free and can be downloaded from the Moscow ML website.

Running Extended ML

On Linux

Type emosml to the shell to run Extended Moscow ML. Then type use "file.eml"; to load the contents of file.eml. Type control-D to quit.

You can use ledit with emosml too; see above for instructions.

If you have a home machine

Extended Moscow ML is free and can be downloaded from here.

Here are a couple of tips on getting the Extended ML system to accept your specifications.

Running QuickCheck

Instructions for running QuickCheck are here. A distribution that is suitable for use under Linux is here. A mildly modified version for Windows of the parts of QuickCheck distribution you need is here.

Reading list

Essential reading

L. Paulson. ML for the Working Programmer, second edition. Cambridge University Press, 1996. Currently £35.15 in paperback (Amazon). The examples in the book are here; answers to selected exercises are here; errata are here.

D. Sannella. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park, 1990. Springer Workshops in Computing, 99-130, 1991. Edinburgh report ECS-LFCS-89-102. Section 4 of this is essential reading. It is available here.

Lecture notes

Paulson's book (see above) and Harper's book and Gilmore's notes (see below) are much better than any brief lecture notes I could produce so for the parts of the course on programming I will not be producing lecture notes. The lecture log tells you what I have covered and the examples log gives you the examples I used. I will however produce a few lecture notes on topics that are not covered in any of these sources.

1. Lazy and eager evaluation
2. Specifying functions in Extended ML
3. Proving that a function meets its specification
4. Specifying structures in Extended ML
5. Proving that a structure meets its specification

Supplementary reading

R. Harper. Programming in Standard ML. Carnegie Mellon University, 2001. This is a free alternative to Paulson's book and I will be following it in most of my lectures on the ML part of the course. However, Paulson's book seems more suitable for learning how to program in ML so that is the one I am recommending. Local copies of Harper's book are available for reading online, with clickable links (but clicking on examples downloads them from CMU, which can be slow), and for printing. A local copy of the examples from the book is here. This is a draft textbook and there are some rough spots. The author would like feedback; please send it to me in the first instance so I can give a quick reaction and filter out any misunderstandings. Please use page numbering as in the printed version, or at least tell me which version you are referring to. Here is a list of errors that I have already noticed or been told about.

S. Gilmore. Programming in Standard ML'97: A tutorial introduction. Edinburgh report ECS-LFCS-97-364, 1997. This is an alternative to Paulson's book for the core ML programming part of the course. The treatment of modules is insufficiently detailed for our purposes. It is available here. A slightly revised version of this is available as hypertext, or for printing.

M. Tofte. Essentials of Standard ML modules. Notes for Summer School on Advanced Functional programming, held at the Oregon Graduate Institute, August, 1996. This is a very nice alternative coverage of the material on ML modules in Paulson's book.

J. Ullman. Elements of ML Programming, second edition. Prentice-Hall, 1997. Currently £41.99 in paperback. This is an alternative to Paulson's book.

R. Harper. Introduction to Standard ML. LFCS report ECS-LFCS-86-14, 1986. This report is a precursor to Harper's textbook. It 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. It is available here.

S. Kahrs. Lecture notes on formal program development. Report ECS-LFCS-97-372, 1997. This is for people who want to know more about the specification part of the course than what is covered in the lectures. It is available here.

Examination

There will be an on-line programming examination during the usual examination period. The examination is closed-book with no access to the internet, but access to the documentation of the Moscow ML library (specifically, this and this) will be available.

Sample exam paper (instructions, solution)

May 2010 exam (instructions)

Standard ML resources

° The Comp.Lang.ML newsgroup and its FAQ ° Moscow ML ° Standard ML of New Jersey ° Poly/ML ° HaMLet, a platform for experimentation with ML variants ° MLj, a compiler taking SML (for now, minus functors) to Java bytecode ° SML.NET, a compiler taking SML to .NET bytecode ° MLserver, a plugin for AOLserver which allows you to write dynamic web applications in SML ° MLton, an SML compiler which generates standalone executables and has a good foreign function interface to C ° A Gentle Introduction to ML ° Tips for Computer Scientists On Standard ML (Revised) ° Extended ML ° SML-mode for Emacs °

Some papers for background reading

° How ML Evolved, Robin Milner ° A Standard ML Compiler, Andrew Appel and Dave MacQueen ° Standard ML of New Jersey, Andrew Appel and Dave MacQueen ° A run-time system, Andrew Appel ° A Critique of Standard ML, Andrew Appel ° A Tutorial on Co-induction and Functional Programming, Andrew Gordon ° Simple Imperative Polymorphism, Andrew Wright ° Principal type-schemes for functional programs, Luis Damas and Robin Milner ° Type Systems, Luca Cardelli ° A semantics for ML concurrency primitives, Dave Berry, Robin Milner and David Turner ° A tutorial on the universality and expressiveness of fold, Graham Hutton °

What does ML have to do with the real world?

Some real-world applications of functional programming

Related languages

° CAML, Objective CAML (a variant of CAML plus objects and classes) and JoCaml (an experimental extension of Objective CAML with high-level communication and synchronising channels and mobile agents) ° Haskell, a lazy functional language ° ATS, an extension of ML with linear types and restricted dependent types ° Alice, an extension of ML with support for concurrent, distributed, and constraint programming ° Cayenne, a Haskell-like language with dependent types °