[Agda] Implementation of abstract vs. irrelevance

[Andrea Vezzosi]

I've grepped the code a bit and it seems that the speedup was mainly
because abstract definitions are skipped by the termination checker [1],
hence avoiding the instantiation of metavariables.

In my case a syntax for non-recursive definitions would solve the slowdown,
but it seems like a better solution could be to teach the termination
checker how to share work between different instantiations of the same
metavariable, if that's possible.

The code:
https://github.com/Saizan/categories/blob/abstract/Categories/Adjunction.agda
[1] https://code.google.com/p/agda/issues/detail?id=847


On Mon, May 13, 2013 at 1:45 PM, Andreas Abel <andreas.abel at ifi.lmu.de>wrote:

> Hi Andrea,
>
> "abstract" means that this definition is only expanded when checking other
> "abstract" definitions.
>
> Irrelevant arguments are not compared during equality checking, however,
> they might still be computed for other reasons, e.g. to determine their
> precise set of free variables.  Substitution also has to traverse
> irrelevant arguments, due to the lack of explicit substitutions in the Agda
> engine.
>
> The implementation of these features is scattered all over the Agda engine
> (TypeChecking.*), you might wanna grep for "AbstractMode" and "releva" to
> get to interesting source locations.
>
> Cheers,
> Andreas
>
>
> On 12.05.2013 12:00, Andrea Vezzosi wrote:
>
>> Hi,
>>
>> I've noticed some very promising speedups by making definitions abstract
>> in addition to irrelevant and I'd like to understand why.
>>
>> Skimming the code I couldn't figure out where the main pieces of the
>> implementation of these features are, is there a commentary on how they
>> are implemented? And what work does abstract save on top of irrelevance?
>>
>>
>> Thanks,
>>     Andrea
>>
>>
>>
>> ______________________________**_________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/**mailman/listinfo/agda<https://lists.chalmers.se/mailman/listinfo/agda>
>>
>>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~**abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20130513/1fc66c40/attachment.html