[Agda] Re: Agda reflection overhaul

[Jesper Cockx]

Hi Ulf,

This looks very nice and useful, I'm looking forward to experimenting with
the new features when I have time. Meanwhile, I tried to convert some of my
code that uses reflection a lot, here are my remarks:

- I don't really understand how I would use extendContext and inContext,
can you give an example?
- Since typeError expects a String, maybe it would be useful to have some
functions for pretty-printing terms/types? Or alternatively we could have a
richer type for error messages.
- There seems to be a problem with either unquoteDef (expects an argument
of type TC T) or deriveEqDef in the prelude (returns a TC (List Clause)).
- Some functions that used to be pure are now integrated into the TC monad,
which causes a lot of my code to become monadic as well. I'm mainly talking
about getType (previously typeOf), getDefinition (previously definitionOf),
getParameters and getConstructors. Would it be possible to keep these
functions pure?
- One thing I noticed when converting my pure code to monadic code
(probably has nothing to do with this change): you cannot combine two
monadic computations at different universe levels (at least with the
definition of monad in the prelude). This is rather annoying, especially
since I don't know a workaround.

cheers,
Jesper

ps: A funny thing happened last year when the agda repository was deleted
and recreated on github, causing all forks to use masondesu/agda as their
new base. I saw this happened with your fork as well. Unfortunately, the
only solution I found was to delete and recreate my fork of agda/agda on
github.

On Fri, Jan 15, 2016 at 11:58 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> I recently had the privilege to sit on David Christiansen's PhD committee,
> and thus had an excuse to take a closer look at what he's been doing with
> elaborator reflection in Idris. Basically what he's done is expose an
> interface to the proof engine to Idris metaprograms. It is very cool and
> lets you do things like backtracking and generating helper functions in
> tactic scripts. So, obviously, I had to steal it.
>
> It's all implemented in a branch on my Agda fork [1] and you can look at
> the release notes here [2]. Briefly, what I've done is add a new primitive
> monad TC with a bunch of primitive operations corresponding to operations
> on TCM in the Agda implementation. For instance,
>
>   catchTC : ∀ {a} {A : Set a} → TC A → TC A → TC A
>   unify : Term → Term → TC ⊤
>   newMeta : Type → TC Term
>   freshName : String → TC QName
>   etc.
>
> The unquote and unquoteDecl/Def primitives then expects TC computations
> instead of pure values, which enables a lot more interesting metaprograms
> than what we had before. A nice side-effect is that I could get rid of the
> reflection primitives (quote-goal etc) from the reflected Term data type.
>
> The idea is that we can get rid of most of the old primitives (quoteGoal,
> quoteContext, tactic) since that functionality is provided by the TC
> operations.
>
> I have updated agda-prelude [3] to the new framework and it seems to work,
> but I would be interested in feedback from people doing lots of reflection
> stuff (you know who you are) before merging this into master.
>
> / Ulf
>
> [1] https://github.com/UlfNorell/agda/tree/new-reflection
> [2]
> https://github.com/UlfNorell/agda/blob/new-reflection/doc/release-notes/2-5-1.txt#L383
> [3] https://github.com/UlfNorell/agda-prelude/tree/new-reflection
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160115/6b794a38/attachment.html