The Laboratory for Foundations of Computer Science at the University of Edinburgh and SICSA present: 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 dependently-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.

This course receives financial support from the Complex Systems Engineering theme of SICSA, the Scottish Informatics and Computer Science Alliance.

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 earlier introductory Agda course held in Edinburgh can be found at:

• http://www.cl.cam.ac.uk/~ok259/agda-course
• https://personal.cis.strath.ac.uk/conor.mcbride/pub/dtp/

Location:

• Lab sessions will take place in 4.12, Appleton Tower

• Labs will start on 14 November and run every week

• Lectures will take place in room 2.33, Informatics Forum

• Lectures will start on 14 November and run (roughly) every 2 weeks (see schedule below)

Course Material:

All course material will be available online.

• Lecture notes
• Code repository

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

git pull origin

Registration and organization:

Please let us know you are coming so we can prepare accordingly:

• Danel Ahman < D.Ahman {ät} ed.ac.uk >
• Sam Lindley < Sam.Lindley {ät} ed.ac.uk >

Mailing List:

Course announcements, discussions and questions are welcome in the agda-course-13 {ät} inf.ed.ac.uk mailing list. Non-registrants: you are welcome to join too, please email Danel or Sam in the addresses above to join, with some indication you are not a machine.

Schedule:

14:00-15:00: Lab session (labs run every week from 14 November)

15:00-15:30: Break

15:30-16:30: Lecture

16:30-17:00: Break

17:00-18:00: Lecture

18:00-…: Pub…

Lecture plan:

1. 14 November, 2013: Introduction via Vectors

2. 28 November, 2013: Metaprogramming the Simply-Typed λ-Calculus

3. 12 December, 2013: Containers and W-Types

4. 16 January, 2014: Indexed Containers

5. 30 January, 2014: Induction-Recursion

6. 20 February, 2014: Observational Equality

7. 3 April, 2014: Type Theory in Type Theory