[Agda] type check cost for `open'

[Sergei Meshveliani]

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