Date(s) - 28/11/2013
2:00 pm - 6:00 pm
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.
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:
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)
All course material will be available online.
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@ed.ac.uk >
Sam Lindley < Sam.Lindley@ed.ac.uk >
Course announcements, discussions and questions are welcome in the email@example.com 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.
14:00-15:00: Lab session (labs run every week from 14 November)
14 November, 2013: Introduction via Vectors
14 November, 2013: Metaprogramming the Simply-Typed λ-Calculus
28 November, 2013: Containers and W-Types
28 November, 2013: Indexed Containers
12 December, 2013: Induction-Recursion I
12 December, 2013: Induction-Recursion II
(TBA): Observational Equality
(TBA): Type Theory in Type Theory