Course pages 2016–17

# 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

(**See also** *Exercise 0* on
the assessment page.)

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:

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

There is a mailing list for the course: **[Javascript required]**.

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 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 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 19 January 2017 (12pm, FS07)
- Introduction. The lambda calculus

*Jeremy Yallop*

Slides

Lecture notes - Monday 23 January 2017 (12pm, FS07)
- The lambda calculus (continued)
*Jeremy Yallop*

Slides

Lecture notes: see notes for 19 January - Thursday 26 January 2017 (12pm, FS07)
- Type inference

*Jeremy Yallop*

Slides

Lecture notes

Online notebook - Monday 30 January 2017 (12pm, FS07)
- The Curry-Howard correspondence
*Neel Krishnaswami*

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 2 February 2017 (12pm, FS07)
- Abstraction and parametricity
*Leo White*

Slides

Lecture notes - Monday 6 February 2017 (12pm, FS07)
- Abstraction and parametricity
*Leo White*

Slides: see slides for 2 February

Lecture notes: see notes for 2 February - Thursday 9 February 2017 (12pm, FS07)
- Abstraction and parametricity
*Leo White*

Slides

Lecture notes - Monday 13 February 2017 (12pm, FS07)
- Generalized algebraic data types (GADTs)
*Jeremy Yallop*

Slides

Lecture notes

Online notebook with code from the lecture - Thursday 16 February 2017 (12pm, FS07)
- GADTs (continued); Application: a typed foreign function interface
*Jeremy Yallop*

Slides (GADTs)

Slides (foreign functions)

Lecture notes: see notes for 13 February

Online notebook

Further reading:*A modular foreign function interface* - Monday 20 February 2017 (12pm, FS07)
- Modular implicits

*Jeremy Yallop*

Slides

Online notebook with code from the lecture

The following commands install a compiler with modular implicits support:

`opam switch 4.02.0+modular-implicits`

Further reading:

eval $(opam config env)

*Modular implicits* - Thursday 23 February 2017 (12pm, FS07)
- Monads etc.
*Jeremy Yallop*

Slides

Lecture notes - Monday 27 February 2017 (12pm, FS07)
- Generic programming
*Jeremy Yallop*

Slides

Online notebook - Thursday 2 March 2017 (12pm, FS07)
- Monads etc. (continued)

Slides

Lecture notes: see notes for 23 February*Jeremy Yallop* - Monday 6 March 2017 (12pm, FS07)
- Effects, concluded; Staging

Slides (effects)

Slides (staging)

Online notebook (staging)

Supplementary notes on effects*Jeremy Yallop* - Thursday 9 March 2017 (12pm, FS07)
- Staging (continued)

Slides

Online notebook*Jeremy Yallop* - Monday 13 March 2017 (12pm, FS07)
- Super-advanced functional programming
*Dominic Mulligan*

Slides

Agda code