[9 Jan 2001] DTS introduced the course, explaining the meaning of ``Applicative Programming'' and ``Specification'' and outlining the features of Standard ML (the vehicle used in this course for teaching Applicative Programming) and Extended ML (likewise, for Specification). He briefly introduced some built-in types of SML (bool, int, real, string, char, unit) and their built-in values. Reading: Chapter 1 and Section 2.1 of Gilmore are relevant.
[11 Jan 2001] DTS introduced function expressions and value bindings and explained how to define functions by pattern-matching. DTS explained the use of SML's local ... in ... end and let ... in ... end constructs to hide auxiliary declarations in declarations and expressions respectively, recursive function declarations. He also mentioned the use of and together with rec to obtain mutual recursion. He explained that SML provides some convenient syntactic abbeviations including the keyword fun for defining functions. Reading: Gilmore, Sections 2.2-2.4 and part of 3.5.
[23 Jan 2001] DTS demonstrated the use of induction to prove properties of recursive definitions. He gave an example (radix) of a function that is defined using let ... in ... end where the auxiliary declarations make use of the parameters of the main function, and used this to explain some aspects of scope in SML. He introduced lists and various examples of list-processing functions. Reading: Gilmore, Sections 2.4-2.5 and Chapter 5 through 5.1, minus exceptions.
[26 Jan 2001] DTS presented a few more list-processing functions, concluding with insertion sort. He introduced higher-order functions with examples compose, twice and iter. Reading: Gilmore, sections 5.3.2, 3.3 and 3.4.
[30 Jan 2001] DTS explained the difference between curried functions like + : int * int -> int and uncurried functions like plus : int -> (int -> int), with functions curry and uncurry to convert back and forth. He introduced the idea of using higher-order functions to express common patterns of computation and gave two examples: map, for applying a function to every element of a list; and reduce, which can be instantiated to give functions like sum of the numbers from n to m, square of n, nth power of m, factorial of n, and the n-term approximation of e to the power x. Reading: Gilmore, sections 3.3 and 3.1.
[2 Feb 2001] DTS presented some additional convenient syntactic abbeviations that are provided by SML: case, if-then-else, andalso and orelse. He then began a discussion of SML's type system, explaining that SML is strongly- and statically-typed, types are automatically inferred and can be polymorphic, and that a well-typed program is guaranteed to be free of run-time type errors. He explained why all of these are Good Ideas. Reading: Gilmore, section 3.5 and the introduction to chapter 4.
[6 Feb 2001] DTS explained polymorphic types and the built-in polymorphic types of records and lists. He explained how new types can be defined by the user using type abbreviations and datatype definitions, and how the latter fit naturally with pattern-matching function definitions. He explained that mutually recursive datatype definitions are possible and fit naturally with mutually recursive functions and that constructors can have functions as arguments. The latter is extremely powerful and can (for example) be used to code Russell's paradox in ML, see the web page of examples from the lectures. Reading: Gilmore, chapter 4 through 4.4.
[9 Feb 2001] DTS finally explained patterns properly and covered further aspects of polymorphism: how to infer types, principal types, and the crucial difference between let-bound and fn-bound variables. Reading: Gilmore, chapter 4 starting with section 4.4 and introduction to chapter 3.
[13 Feb 2001] DTS explained how exceptions are raised and handled. He explained structural induction on lists, showed how to use it to prove properties of list-processing functions, and how to derive structural induction principles for other user-defined datatypes from their declarations. Reading: Gilmore, first half of section 5.1, sections 5.2 and 5.6.
[16 Feb 2001] DTS presented equality types and gave some more examples of higher-order list-processing functions: foldl and foldr. He introduced the difference between eager evaluation as in SML and lazy evaluation as in some other functional programming languages. Reading: Gilmore, introduction to section 5.3, section 5.3.3, beginning of chapter 6.
[23 Feb - 16 Mar: I apologize that I didn't update this at the time, and have now forgotten which material was in which lecture!] DTS finished presenting the SML core language. He explained how to program a lazy variant of any SML function using an explicit type of delayed computations coded using functions. Using the same ideas he showed how to program lazy datatypes in SML, including potentially infinite lists, with a program that computes the infinite list of prime numbers as an example. He briefly introduced references, which unify variables and pointers with automatic storage allocation and de-allocation, and explained assignment and sequencing. He mentioned character input/output as provided by the TextIO library structure. Reading: Gilmore, chapters 6 and 8.
DTS introduced the SML module language. He began by motivating the need for modules, discussing the issues in organizing large programs that are tackled by the module language, and making an analogy between values and types in the core language and modules and interfaces in the module language. He outlined the new concepts (structures, signatures, functors), explained how to define structures and signatures, and how/why to attach a signature qualification to a structure, and how structure:signature matching works. Reading: Harper, section "Signatures and structures".
He explained the principle of data abstraction and began to explain how it is supported by the SML module language. Crucial here is the difference between transparent signature constraints, which reveal identity of types even when this information is not recorded in the signature, and opaque signature constraints, which hide this information. Reading: Harper, section "views and data abstraction".
DTS explained functors, which are functions mapping structures to structures. In this context, the issue of sharing arises. Sharing specifications are sometimes required to constrain the permissible parameters to functors, and to specify required sharing between the parameter and result. This completes the SML module language. Reading: Harper, section "hierarchies and parameterization".
DTS introduced the Extended ML specification language. EML is a wide-spectrum language with SML as its executable subset. To focus on the main issues, this part of the course will restrict attention to total functions that return non-exceptional values. DTS outlined what specifications are and why they are considered important, and sketched how to formally develop programs from specifications. Reading: the introduction of Sannella's "Formal program development in Extended ML for the working programmer".
DTS used a series of small examples (square root, matrix inversion, maximum element of a list, string searching) to show how to specify SML functions using axioms. In place of an SML function definition consisting of a list of equations having a left-hand side of the form id(pattern), a function specification may use arbitrary equations, logical connectives and quantifiers. He explained why it is often desirable to use loose specifications to avoid over-specification. He showed how to prove that a function satisfies the axioms which specify it. Reading: Sannella's "Formal specification of ML programs", sections 2 and 3.
DTS showed how to use axioms in signatures to specify structures, and explained the difference between EML logical equality == and SML computational equality =. Using a structure binding with a question mark as a placeholder for the structure body gives a specification of a yet-to-be-implemented structure. Using a structure body with question marks in type or function definitions gives a partial implementation. He sketched how to show that a structure satisfies a signature containing axioms. If the structure contains substructures then in reasoning about the rest of the structure it is important to refer to the axioms which specify these rather than the code. He showed how to specify functors, which is like specifying structures except that there is an input signature as well as an output signature. Then proving that a functor meets its specification is just a matter of showing that its body meets the output signature under the assumption that its parameter meets the input signature. DTS handed out a summary of what was covered in the course and what students are expected to have learned. Reading: Sannella's FPD in SML for the WP, section 3, and "Formal specification of ML programs", sections 4 and 5.