| dc.description.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. | |
