Dependently typed metaprogramming (in Agda)
Dependently typed functional programming languages such as Agda are capable of expressing very precise types for data. When those data themselves encode types, we gain a powerful mechanism for abstracting generic operations over carefully circumscribed universes. This course will begin with a rapid depedently-typed programming primer in Agda, then explore techniques for and consequences of universe constructions. Of central importance are the “pattern functors” which determine the node structure of inductive and coinductive datatypes. We shall consider syntactic presentations of these functors (allowing operations as useful as symbolic differentiation), and relate them to the more uniform abstract notion of “container”. We shall expose the double-life containers lead as “interaction structures” describing systems of effects. Later, we step up to functors over universes, acquiring the power of inductive-recursive definitions, and we use that power to build universes of dependent types.
Prerequisites: This class assumes familiarity with typed functional programming, but will not require prior experience with depedently-typed programming nor with Agda.
We do, however, recommend dabbling with Agda in advance. Materials from an introductory Agda course can be found at
This course was given at the University of Cambridge Computer Laboratory
All course material will be available online.
After cloning the initial repository, don’t forget to pull the latest changes:
git pull origin
Course announcements, discussions and questions are welcome in the agda-course-2013 mailing list. Non-registrants: you are welcome to join too, please email Ohad in the address above to join, with some indication you are not a machine.
14:00-14:20: Coffee Break
15:20-15:40: Coffee Break
16:40-17:00: Coffee Break
05 August, 2013: Introduction via Vectors
05 August, 2013: Metaprogramming the Simply-Typed λ-Calculus
07 August, 2013: Containers and W-Types
07 August, 2013: Indexed Containers
26 August, 2013: Induction-Recursion I
26 August, 2013: Induction-Recursion II
28 August, 2013: Observational Equality
28 August, 2013: Type Theory in Type Theory
Thanks to Alan Mycroft for arranging the funding! And, of course, to Conor for preparing the course!