[Agda] More powerful quoting & reflection?

[James Deikun]

On Thu, 2012-06-21 at 16:00 +0200, Paul van der Walt wrote:
> Dear readers,
> 
> I am currently looking at what neat tricks can be done with the
> new reflection API, and something I would like to be able to do
> (inspired by the same thing using Template Haskell)
> automatically generate embedding & projection functions for a
> sum-of-products generic programming approach, given some data
> definition.
> 
> It seems the Reflection module contains functions suggestively
> named `constructors`, for example, but I don't know how to use
> them, and they're not (yet) documented. Does anyone know the
> status of these features? Are they usable yet? Also, can I
> create (/modify) a function programatically then splice it back?

Currently the main limitations of reflection are as follows:

1) The generative side of reflection cannot create definitions, only
terms (via unquote and the Term type).  One effect of this is there is
no way to do generic pattern-matching (pattern-matching is only allowed
in definitions; pattern-matching lambdas desugar into local
definitions).  You can of course use pre-built eliminators, but:

2) There is no way to pass a type and its associated reflective codes
(names, terms, definitions) with the assurance that they are compatible.
A function that takes an abstract type only sees the type parameter as a
variable, and there is no way to typecheck unquotes or other ways of
using the codes in context.  The only way out of this is to return raw
Terms to be unquoted and typechecked in the caller's context, which
means in particular there's not much useful you can do by parameterizing
modules on Term and friends.  But if you're willing to work around this,
then:

3) Reflection can only inspect certain types of definitions.  In
particular it cannot inspect function/value definitions other than to
determine their types, nor can it determine field accessors or
constructors for record types.  Inductive datatypes, however, have
pretty complete inspection, although it is as you noticed not very
well-documented.

These limitations made datatype-generic programming with reflection a
nonstarter for me at this point in time; your mileage may vary depending
what you're trying to accomplish and how determined you are.  Your best
bet for figuring out what's what is to read the source of the stdlib's
Reflection module to figure out what types and operations are available
and experiment a bit.