105

Dependently-Typed Metaprogramming (in Agda)

  • Ohad Kammar
  • 8 videos
  • 1,140 views
  • Last updated on Jun 1, 2014
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.

Course materials (lecture notes, exercises) are available from the course's webpage:
http://www.cl.cam.ac.uk/~ok259/agda-course-13/
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 circumsc...
Play all

Loading...

to add this to Watch Later

Add to

Loading playlists...