Course pages 2014–15

# Advanced Functional Programming

#### Mailing list

There is a mailing list for the course: **cl-acs-28@lists.cam.ac.uk**.

Announcements, questions and discussion. Feel free to post!

Have a question but feeling shy? Mail a lecturer instead and we'll
anonymise and post your question: **jeremy.yallop@cl.cam.ac.uk**
or **leo.white@cl.cam.ac.uk**.

#### 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.

#### Tentative lecture schedule

- Thursday 15 January 2015
- Introduction. The lambda calculus

*Jeremy Yallop*

Slides

Lecture notes - Monday 19 January 2015
- The lambda calculus (continued)

*Jeremy Yallop*

Slides

Online Fω interpreter (example files: nats.f perfect.f equality.f)

(Lecture notes: see notes for Thursday 15 January.) - Thursday 22 January 2015
- Type inference

*Jeremy Yallop*

Slides

Online notebook

Lecture notes - Monday 26 January 2015
- The Curry-Howard correspondence

*Jeremy Yallop*

Slides

The Part II Types course is a less-advanced course covering ML, System F and the Curry-Howard correspondence.

- Thursday 29 January 2015
- Abstraction and parametricity part 1

*Leo White*

Slides

Lecture notes - Monday 2 February 2015
- Abstraction and parametricity part 2

*Leo White*

Slides

(Lecture notes: see notes for Thursday 29 January.) - Thursday 5 February 2015
- Abstraction and parametricity part 3

*Leo White*

Slides

(Lecture notes: see notes for Thursday 29 January.) - Monday 9 February 2015
- Generalized algebraic data types (GADTs)

*Jeremy Yallop*

Slides

Online notebook

Lecture notes - Thursday 12 February 2015
- Generalized algebraic data types (GADTs) (continued)

*Jeremy Yallop*

Slides

Online notebook

(Lecture notes: see notes for Monday 9 February.) - Monday 16 February 2015
- Rows

*Leo White*

Slides

Lecture notes - Thursday 19 February 2015
- Monads etc.

*Jeremy Yallop*

Slides

Online notebook

Lecture notes - Monday 23 February 2015
- Monads etc. (continued)

*Jeremy Yallop*

Slides

(Lecture notes: see notes for Monday 19 February.) - Thursday 26 February 2015
- Generic programming

*Jeremy Yallop*

Slides

Online notebook - Monday 2 March 2015
- Staging

*Jeremy Yallop*

Slides

Online notebook - Thursday 5 March 2015
- Staging (continued)

*Jeremy Yallop*

Slides

Online notebook: part 1

Online notebook: part 2 - Monday 9 March 2015
- Applying functional programming at scale with unikernels

*Anil Madhavapeddy*

Slides