Home

Dependently-Typed Metaprogramming (in Agda)

Conor McBride gave an 8-lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:

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.

The lecture notes, code, and video captures are available online.

As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging.

By Ohad Kammar at 2013-08-30 07:34 | Category Theory | Functional | Lambda Calculus | Meta-Programming | Paradigms | Semantics | Teaching & Learning | Theory | Type Theory | other blogs | 18373 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Feedback

Shouldn't zero from exercise 1.5 have type (Fin zero)? (Edit: Wrong, see Jeremy's comment below)

On page 11, I read nInj as lowercase NLNJ and couldn't figure out what it meant.

Also, the precedence of the inversion ^-1 operator was confusing. In the definition of nCase, I assume that's supposed to be (nInj F G)^-1 and not G^-1?

(Edit: Changed the title from Errata, since the only thing I've found wrong was itself wrong.)

By Matt M at Fri, 2013-08-30 13:59 | login or register to post comments

C-style indexing

Fin n is a type with n members, useful for indexing vectors of length n. For example, Fin (suc zero) has one member:

   zero : Fin (suc zero)

and Fin (suc (suc zero)) has two members:

   zero : Fin (suc (suc zero))
   suc zero : Fin (suc (suc zero))

Fin zero should be uninhabited, so we don't want to make zero a member. The actual type of zero makes it a member of Fin n for every positive n (so it serves as the first index into every non-empty vector).

By Jeremy at Fri, 2013-08-30 14:46 | login or register to post comments

Oh right

Oh right, (Fin n) is "Nat less than n". Thanks.

By Matt M at Fri, 2013-08-30 14:51 | login or register to post comments

Great set of notes

I've only skimmed this so far, but this looks like a great resource (especially for a type theory dilettante such as myself). Chapter 7 felt a little rushed, though. I look forward to see that fleshed out.

By Matt M at Fri, 2013-08-30 15:51 | login or register to post comments

Friday afternoon!

I first read the title as "Dependently-Typed Metaprogramming (in Ada)", which sounded pretty interesting to me!

By johnwcowan at Fri, 2013-08-30 16:24 | login or register to post comments