The general aim of the course is to introduce the functional style
of programming using the programming language Standard ML (SML).
Specifically, the course will introduce, illustrate, and examine
the principles of functional programming using key features of SML:
structured datatypes, higher-order functions, and type inference.
Throughout the course applications will be demonstrated via case
studies.
Lectures
Overview and motivation.
Functional programming. Expressions and values. Functions.
Recursion. Types.
Introduction to SML.
SML/NJ and Moscow ML. Value declarations. Static binding.
Basic types: integers, reals, truth values, characters, strings.
Function declarations. Overloading. Types. Recursion.
Expression evaluation. Call-by-value.
Functions and lists.
Types. Polymorphism. Curried functions. Nameless functions.
Lists. Pattern matching. Case expressions. List manipulation.
Tail recursion. Accumulators. Local bindings.
Higher-order functions.
Higher-order functions. List functionals.
Datatypes.
Records. Enumerated types. Polymorphic datatypes. Option type.
Disjoint-union type. Abstract types. Error handling. Exceptions.
Recursive datatypes.
Lists, trees, lambda calculus. Tree manipulation. Tree listings:
preorder, inorder, postorder. Tree exploration: breadth-first and
depth-first search. Polymorphic exceptions. Isomorphisms.
Data structures.
Tree-based data structures. Binary search trees. Red/black trees.
Flexible functional arrays. Heaps. Priority queues.
Lazy datatypes.
Call-by-value, call-by-name, and call-by-need evaluation. Sequences,
streams, trees. Lazy evaluation. Sieve of Eratosthenes.
Breadth-first and depth-first traversals.
Program specification and verification.
Testing and verification. Rigorous and formal proofs. Structural
induction on lists. Law of extensionality. Multisets. Structural
induction on trees.
Objectives
At the end of the course students should
be familiar with key concepts of programming in a functional style
be able to develop software in SML in a competent manner
understand how to use the typing discipline for clearer and
verifiable programs
Recommended reading
Books:
* Paulson, L.C. (1996). ML for the working programmer. Cambridge University Press.
* Okasaki, C. (1998). Purely functional data structures. Cambridge University Press.
Papers:
Backus, J. (1978). Can programming be liberated from the von Neumann style? A functional style and its algebra of programs. Communications of the ACM, vol. 21, pp. 613-641.
Landin, P.J. (1966). The next 700 programming languages. Communications of the ACM, vol. 9, pp. 157-166.
