The Logic, Semantics, and Programming Languages Group at the University of Cambridge presents:

Dependently typed metaprogramming (in Agda)

Conor McBride

MSP, University of Strathclyde

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

http://www.cl.cam.ac.uk/~ok259/agda-course and

https://personal.cis.strath.ac.uk/conor.mcbride/pub/dtp/

Location:

This course was given at the University of Cambridge Computer Laboratory

Course Material:

All course material will be available online.

• Lecture notes.

• Repository: https://github.com/pigworker/MetaprogAgda

After cloning the initial repository, don’t forget to pull the latest changes:

git pull origin

• Video captures

Mailing List:

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.

Schedule:

13:00-14:00: Laboratory

14:00-14:20: Coffee Break

14:20-15:20: Lecture

15:20-15:40: Coffee Break

15:40-16:40: Lecture

16:40-17:00: Coffee Break

17:00-18:00: Laboratory

18:00-…: Pub…

Past Lectures:

1. 05 August, 2013: Introduction via Vectors
   Location: SW01
   Video

2. 05 August, 2013: Metaprogramming the Simply-Typed λ-Calculus
   Location: SW01
   Video

3. 07 August, 2013: Containers and W-Types
   Location: SW01
   Video

4. 07 August, 2013: Indexed Containers
   Location: SW01
   Video

5. 26 August, 2013: Induction-Recursion I
   Location: SW01
   Video

6. 26 August, 2013: Induction-Recursion II
   Location: SW01
   Video

7. 28 August, 2013: Observational Equality
   Location: SW01
   Video

8. 28 August, 2013: Type Theory in Type Theory
   Location: SW01
   Video

Acknowledgements

Thanks to Alan Mycroft for arranging the funding! And, of course, to Conor for preparing the course!