This post is about adapting descriptions, used to encode dependently typed datatypes (including type families) originally in The Gentle Art of Levitation, to inductive-recursive types.

Before jumping straight into implementing datatypes via descriptions, it is convient to be able model some of them in Agda (as done in The Gentle Art of Levitation by Chapman et. al. and subsequent papers). Everything in the surface language, such as datatype declarations and pattern matching, is elaborated to terms of the core type theory. It is desirable to have the ingredients of the core type theory be as similar to their higher level counterparts as possible, otherwise work on the canonical terms (such as embedding back upwards, generic programming on core terms, and compilation of core terms) becomes complex.

Since becoming a PhD student at Portland State, I’ve been occasionally hacking on what is currently a rather boring type checker (by the name of Spire), but what I hope to become a dependently typed language for experimenting with generic programming. Development has been slow and sporadic, so for the new year I’m going to try out this daily development blog.