15-150: Functional Programming, Spring 2012

This is an archive of the Spring 2012 version of 15-150, taught by Dan Licata. This spring semester was the most polished version of the three times I taught the course, Spring 2011, Fall 2011, and Spring 2012. I designed 15-150 with Robert Harper, along with the Spring 2011 TAs, Ian Voysey, Michael Arntzenius, Arbob Ahmad, and Zach Sparks.

Overview

The purpose of this course is to introduce the theory and practice of functional programming (FP). The characteristic feature of FP is the emphasis on computing by calculation. The traditional distinction between program and data characteristic of imperative programming (IP) is replaced by an emphasis on classifying expressions by types that specify their behavior. Types include familiar (fixed and arbitrary precision) numeric types, tuples and records (structs), classified values (objects), inductive types such as trees, functions with specified inputs and outputs, and commands such as input and output. Execution of imperative programs is generalized to evaluation of well-typed expressions by a smooth extension of mathematical experience to programming practice.

The advantages of FP are significant:

• Verification: There is a close correspondence between the reasoning that justifies the correctness of a program and the program itself. Principles of proof by induction go hand-in-hand with the programming technique of recursion.
• Parallelism: Evaluation of compound expressions is naturally parallel in that the values of subexpressions may be determined simultaneously without fear of interference or conflict among them. This gives rise to the central concepts of the work (sequential) and span (idealized parallel) complexity of a program, and allows programs to exploit available parallelism without fear of disrupting their correctness.
• Abstraction: FP stresses data-centric computation, with operations that act on compound data structures as whole, rather than via item-by-item processing. More generally, FP emphasizes the isolation of abstract types that clearly separate implementation from interface. Types are used to express and enforce abstraction boundaries, greatly enhancing maintainability of programs, and facilitating team development.

Moreover, FP generalizes IP by treating commands as forms of data that may be executed for their effects on the environment in which they occur. Upon completion of this course, students will have acquired a mastery of basic functional programming technique, including the design of programs using types, the development of programs using mathematical verification techniques, and the exploitation of parallelism in applications.

Prerequisites: 21-127: Concepts of Mathematics, or permission of instructor. Students will require some basic mathematical background, such as the ability to do a proof by mathematical induction, in order to reason about program correctness.

Successful completion of this course is necessary and sufficient for entry into 15-210 Data Structures and Algorithms, which will build on the functional model of computation to develop a modern account of parallel algorithms for a wide variety of abstract types.