Aims

This module shows how to use the features of modern typed functional programming languages such as OCaml, Haskell and Agda to design and implement libraries and DSLs. It introduces a variety of programming techniques for improving both correctness and efficiency.

Students wishing to take the module should have some experience of a typed functional programming language and an understanding of type inference.

Syllabus

Part 1: Types in functional languages.

• Typed lambda calculi. Beyond Hindley-Milner type inference. The Curry-Howard correspondence.
• Higher-rank polymorphism. Duality of existentials and universals. Parametricity and abstraction.
• Modules, signatures, and functors.
• Phantom types and generalised algebraic data types.
• Implicit arguments and overloading
• Dependent types

Part 2: Programming in functional languages.

• Monads and related abstractions.
• Algebraic effects
• Datatype-generic programming.
• Staging and metaprogramming.

Objectives

On completion of this module students should be able to:

• Understand the elements of type systems used in modern typed functional programming languages (e.g. OCaml, Haskell, Agda).
• Apply modern approaches to designing libraries and DSLs, with appropriate use of monads, applicative functors, effects and related abstractions.
• Use advanced type system features to specify precise typed interfaces.
• Understand how to use metaprogramming to improve performance.

Coursework

Coursework will consist of three take-home problem sets.

Practical work

In addition to the take-home problem sets there will be (unassessed) interactive exercises to accompany many of the lectures.

Assessment

Three take-home problem sets, each accounting for approximately a third of the marks.

Recommended reading

Minsky, Y. & Madhavapeddy, A. and Hickey, J. (2013). Real World OCaml. O'Reilly Media (1st edition). (Also available online.) We'll assume familiarity with the concepts introduced in chapters 1--6.
Pierce, B. C. (2002). Types and Programming Languages. The MIT Press (1st edition). Pierce's book will be a useful reference for some of the concepts introduced in the first half of the course, although we'll be taking a less formal approach.