Course pages 2017–18
Advanced Functional Programming
Mailing list
There is a mailing list for the course: [Javascript required].
The mailing list is used for announcements, questions and discussion. Feel free to post!
Have a question but feeling shy? Mail the lecturer instead ([Javascript required]) and I'll anonymise and post your question.
Preparation
We'll be using (mostly) OCaml and (some) Agda in the course. The following books provide sufficient background:

OCaml from the Very Beginning
John Whitington
Available in print, or as a PDF ($14.99) 
Real World OCaml
Yaron Minsky, Anil Madhavapeddy, Jason Hickey
Available in print, or online. Chapters 1 to 6 give enough background for this course.
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 MLfamily 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 LambdaCalculus) and 9 (Simply Typed LambdaCalculus) 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 lessadvanced course covering ML, System F and the CurryHoward correspondence.
Tools
The OPAM package manager is the recommended way to install OCaml.
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 advancedfp git://github.com/ocamllabs/advancedfprepo
$ opam install fomega
The interpreter can also be used directly in the browser.
Tentative lecture schedule
 Thursday 18 January 2018 (12pm, SW01)
 Lambda calculus (I)
Jeremy Yallop
Slides (introduction)
Slides (lambda calculus)
Lecture notes
Syntax reference
 Monday 22 January 2018 (12pm, SW01)
 Type inference
Nada Amin
Slides
Lecture notes
Interactive online notebook
 Thursday 25 January 2018 (12pm, SW01)
 Abstraction and parametricity (I)
Slides
Lecture notes
Nada Amin
 Monday 29 January 2018 (12pm, SW01)
 Lambda calculus (II)
Jeremy Yallop
Slides
Lecture notes
 Thursday 1 February 2018 (12pm, SW01)
 Abstraction and parametricity (II)
Nada Amin
Slides
Lecture notes
 Monday 5 February 2018 (12pm, SW01)
 The CurryHoward Correspondence
Nada Amin
Slides
Recommended additional reading: Propositions as Types (Philip Wadler, 2015)
Further reading: Lectures on the CurryHoward isomorphism (Morten Heine B. Sørensen and Paweł Urzyczyn, 1998)  Thursday 8 February 2018 (12pm, SW01)
 Indexed data (I): generalized algebraic data types
Jeremy Yallop
Slides
Lecture notes
Online notebook with code from the lecture  Monday 12 February 2018 (12pm, SW01)
 Semirings
Jeremy Yallop
Slides
 Thursday 15 February 2018 (12pm, SW01)
 Generalized algebraic data types, continued; Implicits
Jeremy Yallop
Slides (GADTs)
Slides (Implicits)
Lecture notes (GADTs): see notes from 8 February
Code and notes for modular implicits
Further reading: Modular implicits (Leo White, Frédéric Bour and Jeremy Yallop, 2015)
 Monday 19 February 2018 (12pm, SW01)
 Effects (I): monads etc.
Jeremy Yallop
Slides
Lecture notes
 Thursday 22 February 2018 (12pm, SW01)
 Effects (II): algebraic effects & handlers
Jeremy Yallop
Slides
Supplementary notes on effects
 Monday 26 February 2018 (12pm, SW01)
 Indexed data (II): inductive families
Jeremy Yallop
Slides
Agda code (plain)  Thursday 1 March 2018 (12pm, SW01)
 Generic programming
Jeremy Yallop
Slides
Online notebook
Agda code (plain)  Monday 5 March 2018 (12pm, SW01)
 Multistage programming (I)
Jeremy Yallop
Slides
Online notebook
 Thursday 8 March 2018 (12pm, SW01)
 Multistage programming (II)
Jeremy Yallop
Slides
Online notebook (partiallystatic data)
Supplementary notes (staging and effects)
 Monday 12 March 2018 (12pm, SW01)
 Recursion
Jeremy Yallop
Slides
Supplementary notes on staging and recursion
Further reading: Staged generic programming (2017)