[Agda] Re: Agda reflection overhaul

[Ulf Norell]

On Fri, Jan 15, 2016 at 2:58 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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?
>

See Tactic.Nat.Induction for an example (
https://github.com/UlfNorell/agda-prelude/blob/new-reflection/src/Tactic/Nat/Induction.agda#L40).
When you create a new meta (newMeta) you get a term valid in the current
context, and inferType and checkType does checking relative to the current
context.


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

I'm going for the latter. I have an implementation of an error message type
with string and term constructors that I did before the current overhaul. I
just need to merge it.


> - 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)).
>

You have to use defineFun:

  unquoteDef myEq = defineFun myEq =<< deriveEqDef (quote SomeType)

I only did the minimal changes necessary to get agda-prelude working. With
the new framework many things can be cleaned up and made more useful.


> - 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?
>

Short answer: no. They were already not quite pure. For instance, you could
call definitionOf in a mutual block before you actually have the
definition, but depending on when the call was actually evaluated you may
or may not get the full definition. With the new API things are even worse
since you can create new definitions on the fly (with freshName, declareDef
and defineFun). I guess the parameter and constructor functions could still
be pure, but it felt more consistent to put everything in the monad.


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

There is PMonad type class with a bind function _>>=′_ that accepts things
at different levels. I forgot to make TC an instance though.


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

Huh, I hadn't noticed that. I guess I should sort that out at some point :).

/ Ulf


>
> 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/7163d6d5/attachment.html