[Agda] type check cost for `open'

[Peter Selinger]

Sergei Meshveliani wrote:
> 
> On Mon, 2015-08-17 at 15:52 -0300, Peter Selinger wrote:
> > What would it take to equip Agda with an efficient evaluation
> > strategy?
> 
> 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").

For clarification: I am talking about (1). My interest is in theorem
proving, not in running programs. But theorem proving (or type
checking) often requires the evaluation of terms in the sense of
(1). This leads to extremely long type checking times if the
evaluation is inefficient.

To illustrate my point, consider this example. I am concerned with
proving theorems of the form Γ ⊢ w === v, where w and v are words in
some alphabet, Γ is a set of axioms, and Γ ⊢ w === v means that the
equation follows from the axioms by the laws of monoids.

In my last email, I defined a function

  comm-canonical : List X -> List X

which inputs a word and calculates a canonical representative up to
commutativity. The details of its definition are not important here. 
I use the function comm-canonical to prove the following (meta)-theorem:

  general-commutativity : ∀ {w v : List X} -> comm-canonical w ≡ comm-canonical v -> Γ ⊢ w === v

This theorem can then be used to automate other proofs. Namely, if I
have to show Γ ⊢ w === v where it happens to follow from
commutativity, I can just give

  general-commutativity refl

as the proof term. To check that the "refl" is well-typed, Agda will
automatically calculate the normal forms of the left- and right-hand
sides and check that they are equal.

This sort of automation is essential when doing long proofs, because
proving some general instance of commutativity by applying individual
axioms can get very tedious very fast. 

So it is important for type-checking that a function such as
comm-canonical can be evaluated efficiently. The normal evaluation
order of Agda makes it very difficult to do so. (The solution I gave
in my last email, namely, using continuation passing style, indeed
works.  However, it is not without problems, because proving theorems
about CPS-style functions is not trivial and gives proofs that are
significantly convoluted).

> 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) ...) ?

For the record: yes, if I compile the program with agda -c, it is very
fast, so Haskell lazy evaluation is definitely taking place in that
case. But this does not help at all with evaluation during type
checking, which is what I really need.

> 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. 

Yes, this is exactly the point I was hoping to make! In the example I
gave, O(n^2) turned into O(exponential).

My question remains: what would be involved in equipping Agda with an
efficient evaluation strategy? Could a proficient Haskell programmer
do it by modifying some well-defined set of modules, or would it
require a more pervasive set of changes to the internals of Agda?

-- Peter