[Agda] More powerful quoting & reflection?

[Altenkirch Thorsten]

Hi,

it is clear that the current reflection api is rather a proof of concept,
implemented at one AIM and should be developed further to give access to
definitions etc. Paul's motivation seems to be a good one and I would
suggest that he should maybe propose an API which would address his needs
and we can discuss this here.

Thorsten


On 21/06/2012 17:07, "James Deikun" <james at place.org> wrote:

>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.
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.