<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
(resending to the list; forgot to reply-all the first time around)<br>
<br>
Agda evaluation is quite different from GHC. Agda (mostly? always?)
uses a <a moz-do-not-send="true"
href="https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_name">call-by-name</a>
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: <a
moz-do-not-send="true"
href="https://github.com/m0davis/agda-prelude/blob/a0a9793243630595cee9f158bbd4ba5800e6f9da/src/Tactic/Reflection/Reright-Performance-BestExamples-LambdaLift.agda">lambda
lifting</a> and <a moz-do-not-send="true"
href="https://github.com/m0davis/agda-prelude/blob/a0a9793243630595cee9f158bbd4ba5800e6f9da/src/Tactic/Reflection/Reright-Performance-BestExamples-ContinuationPassingStyle.agda">continuation
passing</a>. I found that --sharing was only necessary for one
case in my lambda-lifting examples. That case was borrowed from Ulf
in <a moz-do-not-send="true"
href="https://github.com/agda/agda/issues/426#issuecomment-129023261">issue
426</a>.
<div class="moz-forward-container">
<p>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!</p>
<br>
<div class="moz-cite-prefix">On 10/01/2016 07:45 AM, Sergei
Meshveliani wrote:<br>
</div>
<blockquote
cite="mid:1475333106.3038.64.camel@one.mechvel.pereslavl.ru"
type="cite">
<pre wrap="">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
<a moz-do-not-send="true" class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a moz-do-not-send="true" class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</div>
</body>
</html>