[Agda] evaluation strategy (was: shared record parts)

[Martin Stone Davis]

(resending to the list; forgot to reply-all the first time around)

Agda evaluation is quite different from GHC. Agda (mostly? always?) uses 
a call-by-name 
<https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_name> 
strategy while GHC (Haskell in general, I think) is lazy. In my own 
project, I've only recently started to figure out how this works and 
have had some success in increasing the speed of typechecking. There are 
two strategies that I know of that were of use to me: lambda lifting 
<https://github.com/m0davis/agda-prelude/blob/a0a9793243630595cee9f158bbd4ba5800e6f9da/src/Tactic/Reflection/Reright-Performance-BestExamples-LambdaLift.agda> 
and continuation passing 
<https://github.com/m0davis/agda-prelude/blob/a0a9793243630595cee9f158bbd4ba5800e6f9da/src/Tactic/Reflection/Reright-Performance-BestExamples-ContinuationPassingStyle.agda>. 
I found that --sharing was only necessary for one case in my 
lambda-lifting examples. That case was borrowed from Ulf in issue 426 
<https://github.com/agda/agda/issues/426#issuecomment-129023261>.

You may want to look through my linked sample code and try to understand 
why some parts typecheck more quickly than others. In the lambda lifting 
one, use C-u C-u C-c C-, in the holes; in continuation passing, use C-c 
C-n. Try to write out the normalisation step-by-step in each case (as I 
did at the bottom of the continuation passing one) until you convince 
yourself that you understand why it typechecks either slowly or quickly. 
Then maybe you can return to your own code and spot the flaws!


On 10/01/2016 07:45 AM, Sergei Meshveliani wrote:
> People,
> I am trying to find the main sources of type checking inefficiency in
> the system of
> (my library for algebra + Agda implementation).
>
> Th investigation with  no-eta-equality + copatterns  has given nothing,
> because the most interesting module is not type-checked, it is difficult
> to understand, why. The module in close to end, the program is complex.
>
>    
> Another suspect is as follows.
> My library has many parts like this:
>
>   -----------------------------------------------------------
>   module (commutativeRing : CommutativeRing _ _)
>     where
>     open CommutativeRing commutativeRing using
>                          (Carrier; *semigroup; *upSemigroup;
>                           *monoid; upRingoid; ring; upRing)
>    
>     f x =  g *semigroup
>
>     f1 x = g1 *monoid
>
>     f2 x = g2 ring
>     ...
>   ------------------------------------------------------------
>
> And the imported record instances  *semigroup; *upSemigroup;
> *monoid; upRingoid; ring; upRing
> present a tower, some of the tower levels include some others as record
> field values.
> These record types also carry some implementation in them.
> Then,  (f x), (f1 x), (f2 x) ...  take as arguments the parts of this
> tower.
> Thus,  f2 analyzes  ring (to some depth),  f analyzes *semigroup (to
> some depth), and *semigroup is a considerable part of this  ring.
> There appears the question of how sharing and laziness work in such
> examples: how eagerly the structure of *semigroup will be copied,
> what happens when this data becomes un-referenced, and so on.
> Is it like in GHC ?
>     
> I program such modules in Agda as I did it in Haskell + GHC for symbolic
> computation and for a term rewriting library. And with GHC, I am sure
> that it this example it will unwind the parts of  ring and *semigroup
> in the lazy style, and with sharing. So that in computation, the term
> data will not blow up to surprise me much. And if it does, then I am
> able to find the source and to fix my program.
> The Agda type checker may evaluate in another way, not similarly to how
> it evaluates a GHC-compiled program.
> So, I wonder.
>
> Regards,
>
> ------
> Sergei
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161003/da98a893/attachment.html