Course pages 2015–16
Advanced Functional Programming
Mailing list
There is a mailing list for the course: [Javascript required].
Announcements, questions and discussion. Feel free to post!
Have a question but feeling shy? Mail the lecturer instead and we'll anonymise and post your question: [Javascript required].
Preparation
If you haven't used a typed functional language before then it would be wise to familiarize yourself with the basics before the course starts. We'll be using OCaml in the course, and recommend starting with either of the following books:
- Real World OCaml
Yaron Minsky, Anil Madhavapeddy, Jason Hickey
Available in print, or online. Chapters 1 to 6 give enough background for this course. - OCaml from the Very Beginning
John Whitington
Available in print, or as a PDF ($14.99)
The OCaml Beginners mailing list is also a useful resource.
The first few lectures are quite theory oriented: we'll be looking at various typed lambda calculi, along with type inference in ML-family languages. If you haven't studied the lambda calculus before then some background reading is likely to make these lectures much easier to follow. There are many introductions available; one which fits well with our approach is
- Types and Programming Languages
Benjamin C. Pierce
There are copies in the Computer Laboratory library and many of the college libraries.
The material in chapters 5 (The Untyped Lambda-Calculus) and 9 (Simply Typed Lambda-Calculus) is essential. We'll also be covering material from later chapters (11, 23, 24, 29, 30), although in much less detail than Pierce.
Additionally, the Part II (third year undergraduate) Types course is a less-advanced course covering ML, System F and the Curry-Howard correspondence.
Tools
Installing the tools beforehand will also make things easier when the course starts.
The Real World OCaml website has instructions for installing the OCaml toolchain.
We will be using System Fω in the course to illustrate theoretical aspects of functional programming. We have provided an Fω interpreter (based on the interpreters by Pierce for the "Types and Programming Languages" book) so you can try out the examples.
The interpreter can be installed using opam with the following instructions:
$ opam remote add advanced-fp git://github.com/ocamllabs/advanced-fp-repo
$ opam install fomega
The interpreter can also be used directly in the browser.
Lecture schedule
- Thursday 14 January 2016 (12pm)
- Introduction. The lambda calculus
Jeremy Yallop
Slides
Lecture notes - Friday 15 January 2016 (10am) (Note unusual time and day!)
- The lambda calculus (continued)
Jeremy Yallop
Slides
Lecture notes: see notes for 14 January - Thursday 21 January 2016 (12pm)
- Type inference
Jeremy Yallop
Slides
Lecture notes
Online notebook - Monday 25 January 2016 (12pm)
- The Curry-Howard correspondence
Jeremy Yallop
Slides
Recommended additional reading: Propositions as Types (Philip Wadler, 2015)
Further reading: Lectures on the Curry-Howard isomorphism (Morten Heine B. Sørensen and Paweł Urzyczyn, 1998) - Thursday 28 January 2016 (12pm)
- Abstraction and parametricity part 1
Leo White
Slides
Lecture notes - Monday 1 February 2016 (12pm)
- Abstraction and parametricity part 2
Leo White
Slides: see slides for 28 January
Lecture notes: see notes for 28 January - Thursday 4 February 2016 (12pm)
- Abstraction and parametricity part 3
Leo White
Slides
Lecture notes - Monday 8 February 2016 (12pm)
- Generalized algebraic data types (GADTs)
Jeremy Yallop
Slides
Lecture notes - Thursday 11 February 2016 (12pm)
- Generalized algebraic data types (GADTs) (continued)
Jeremy Yallop
Slides
Online notebook
Lecture notes: see notes for 8 February - Monday 15 February 2016 (12pm)
- Monads etc.
Jeremy Yallop
Slides
Online notebook
Lecture notes - Thursday 18 February 2016 (12pm)
- Monads etc. (continued)
Jeremy Yallop
Slides
Lecture notes: see notes for 15 February - Monday 22 February 2016 (12pm)
- Generic programming
Jeremy Yallop
Slides
Online notebook - Thursday 25 February 2016 (12pm)
- Staging
Jeremy Yallop
Slides
Online notebook - Monday 29 February 2016 (12pm)
- Staging (continued)
Jeremy Yallop
Slides
Online notebook (1)
Online notebook (2) - Thursday 3 March 2016 (12pm)
- Arrows and reagents
KC Sivaramakrishnan
Slides - Monday 7 March 2016 (12pm)
- Applying functional programming at scale with unikernels
Anil Madhavapeddy