[Agda-dev] One more point for my false-golfing score

[Wolfram Kahl]

On Wed, Jul 01, 2015 at 09:07:17PM +0200, Andreas Abel wrote:
 > On 01.07.2015 17:49, Wolfram Kahl wrote:
 > > If you take out the ``abstract'' and the indentation,
 > > you get a positivity-check error message that sounds like
 > > it might be ``fixed'' even for continued use of ``abstract''...  ;-(
 > 
 > I did not understand what you meant by this.

I just thought that the experts on positivity checking (i.e., you ;-)
would likely be able to just hack the implementation so it does the check
also inside the ``abstract'' block, and then continue from there.

I think the question is: Can we remove ``abstract''?

Are there any use cases where it actually still makes a significant difference?

WHen I abandoned ``abstract'', it just gave me gains in type-checking time
in the order of 1% to 2% on my RATH-Agda code base of the time,
and I started needing some of the proofs anyways.
For one to two percent typechecking time, I think it is not worth the extra complexity.

I also am under the impression that most of the people who are likely to
use ``abstract'' nowadays use irrelevance.

So it is probably best that you ask on the general list whether anybody
actually needs abstract, and ask for constructive proof, i.e.,
code examples where ``abstract'' does make a significant difference,
so you can run tests yourself and quantify the difference.


Cheers,

Wolfram