Spire Language Development Blog

Implementing a language with dependent types!

Modeling Elimination of Described Types

| Comments

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.