[Agda] type check cost for `open'

[Philipp Hausmann]

Hi,

I actually noticed the absence of sharing in Agda as well when working
on the compiler backends. At the moment,
all Agda compiler backends do *not* preserve sharing. The reason is that
sharing is lost when Agda code gets
translated to Agda's Internal syntax, which is used as input for
compilation.

However, the MAlonzo backend mostly gets away with it because GHC is
really clever and re-introduces sharing.
This seems to depend on the GHC version and the optimization level, and
I have no idea if it always works.
So this problem is not really solved with regards to compiling Agda
code, but usually (always?) GHC solves
the problem for us. It's still a problem for all other backends though....

Cheers,
Philipp

On 08/18/2015 02:36 PM, Sergei Meshveliani wrote:
> On Mon, 2015-08-17 at 15:52 -0300, Peter Selinger wrote:
>> Hi all,
>>
>> I'm in the process of formalizing a moderately large project in Agda,
>> and I would like to echo the experience of Sergei and others:
>> reduction performance is a major bottleneck - perhaps the greatest
>> issue standing in the way of making Agda truly useable. 
>>
>> I've been doctoring around with symptoms: introducing a bit of
>> strictness here and there, splitting modules, etc. These workarounds
>> are ugly, never quite solve the problem completely, and sometimes they
>> introduce additional complications and proof obligations.
>>
>> What would it take to equip Agda with an efficient evaluation
>> strategy? For example, would this be as simple as providing an
>> alternate implementation of a handful of modules in the Agda source
>> code? Or is it something that would require deeper modifications
>> throughout the system?
>>
>> Here is an example I was struggling with and just worked out. 
>> I am dealing with word problems in monoids, and I have written a
>> function comm-canonical that inputs a word and outputs a canonical
>> form modulo commutativity of generators. The implementation is
>> correct, but I'm not concerned with correctness at the moment; only
>> with the running time.
>>
>> The 4 functions defined in the module Commuting should in principle be
>> efficient. All of the functions are linear (in the sense that each
>> argument is used exactly once), so there should be no special issues
>> related to evaluation strategy. In principle, the functions split,
>> unsplit, and insert should run in time O(n), and comm-canonical should
>> run in time O(n^2), where n is the length of the list.
>>
>> -- ----------------------------------------------------------------------
>> -- BEGIN CODE
>> -- ----------------------------------------------------------------------
>>
>> [..] ys) x zs
>> -- ----------------------------------------------------------------------
>> -- A trivial example use of Commuting.
>>
>> data Gen : Set where
>>   A : Gen
>>
>> my-comm : (x y : Gen) -> Bool
>> my-comm A A = true
>>
>> my-less : Gen -> Gen -> Bool
>> my-less A A = false
>>
>> open module Commuting-Gen = Commuting Gen my-comm my-less
>>
>> test : ℕ -> List Gen
>> test n = comm-canonical (replicate n A)
>>
>> -- ----------------------------------------------------------------------
>> -- END CODE
>> -- ----------------------------------------------------------------------
>>
>> [..]
>
>> However, testing shows that evaluating the function "test" takes
>> exponential time:
>>
>> test 16: 7 seconds
>> test 17: 15 seconds
>> test 18: 30 seconds
>> test 19: 60 seconds
>>
>> etc.
>>
>> After much investigation (and befuddlement), I realized the source of
>> the problem, which is actually the fact that the function split
>> returns a pair. Because of Agda's normal order evaluation without
>> sharing
>> [..]
>
> Peter,
> you use the word `evaluation'.
> In Agda this word has the two meanings.
>
> (1) Evaluation to the normal form at the stage of type checking a 
>     program.
> (2) Evaluation of the compiled executable program (after "agda -c").
>
> First the program is  type checked,  then it can be compiled, 
> then its executable can be run.
>
> Also it can be run right by (1) -- which often occurs very slow.
>
> In my programs (2) is fast. For example, if the method is expected as
> O(n), then it is so when evaluated at the stage of (2).
> Such is my experience.
>
> Now: after compiling your program by  "agda -c" 
> is its executable evaluation cost order as expected (O(n) ...) ?
>
> And I am complaining on (probably) another effect:
> the performance of the interpreter of (1) effects the performance of
> type-checking. As this stage indeed O(n) may convert to O(n^2) or to
> something larger. The leads to a great cost of type-checking of a
> real-size library written in Agda. 
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda