Reflection in Agda

Abstract

This project explores the recent addition to Agda enabling reflection, in the style of Lisp, MetaML, and Template Haskell. It illustrates several possible applications of reflection that arise in dependently typed programming, and details the limitations of the current implementation of reflection. Examples of type-safe metaprograms are given that illustrate the power of reflection coupled with a dependently typed language. Among other things the limitations inherent in having quote and unquote implemented as keywords are highlighted. The fact that lambda terms are returned without typing information is discussed, and a solution is presented. Also provided is a detailed users' guide to the reflection API and a library of working code examples to illustrate how various common tasks can be performed, along with suggestions for an updated reflection API in a future version of Agda.