Aims

This module shows how to use the features of modern typed functional programming languages such as OCaml and Haskell 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. Hindley-Milner type inference and beyond. The Curry-Howard isomorphism.
• Higher-rank polymorphism. Duality of existentials and universals. Parametricity and abstraction.
• Modules, signatures, and functors.
• Records and variants
• Phantom types and generalised algebraic data types.

Part 2: Programming in functional languages.

• Typeful interfaces and domain-specific languages.
• Monads and related abstractions.
• Datatype-generic programming.
• Staging and metaprogramming.

Objectives

On completion of this module students should be able to:

• Understand extensions to Hindley-Milner type systems common in modern typed functional programming languages (e.g. OCaml, Haskell).
• Apply modern approaches to designing libraries and DSLs, with appropriate use of monads, applicative functors, 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.