[Agda] Performance issues and code structure.

[Dan Doel]

On Sunday 27 September 2009 8:22:59 am Nils Anders Danielsson wrote:
> On 2009-09-27 05:49, Dan Doel wrote:
> > Loading it up using the command line 'agda' command reveals that it's
> > causing a (haskell) stack overflow.
> 
> I run Agda using the following command-line which increases the maximum
> stack size (40M), and introduces a maximum heap size (2G) to avoid
> swapping:
> 
>   agda +RTS -M2G -K40M -RTS
> 
> In Emacs I have set haskell-ghci-program-args to '("+RTS" "-M2G" "-K40M"
> "-RTS").
> 
> > Is it the equational reasoning that's so expensive?
> 
> Probably not, but maybe it exacerbates the problem. You could try
> replacing all the inferable code with underscores.
> 
> The Agda typechecker normalises code before checking equality. If the
> normalised terms are large, then equality checking can be slow. Note
> that records are η-expanded, and that sharing is /not/ preserved by
> Agda's current call-by-name evaluator. Furthermore I believe that
> lambda-lifting is performed before type-checking, which means that a
> module (record) header's telescope is prepended to every definition
> inside the module, thus causing even more equality checking to be
> performed.

Well, in the course of fooling with various things, I managed to make this 
code much more efficient. I'm still not entirely sure why this happens, 
though. I'll describe it briefly here:

My notion of a product in a category is a record:

  record _Product (C : Category) (A B : Cat.Obj C) : Set where
    ...
    field
      A×B   : Obj

      ... morphisms and laws

Then, the fact that a category has all binary products is represented by 
another record:

  record _Has-Products (C : Category) : Set where
    ...
    field
      has-product : ∀{A B} → (C Product) A B

    infixr 65 _×_
    _×_ : Obj → Obj → Obj
    A × B = _Product.A×B {C} (has-product {A} {B})

    private
      module Local {A B : Obj} where
        open _Product {C} (has-product {A} {B}) public

    ...

This is the version that performs acceptably with all the proofs. The version 
that was using all my memory and then overflowing the stack omitted those two 
{C}s when opening _Product.

The way I discovered this was quite roundabout. Everything looks fine without 
the {C}s normally. However, for an unrelated matter, I wanted to see what 
having a proof-irrelevant equality would be like. When I enacted that, 
_Product turned yellow in those two situations, and I had to fill in {C}. This 
in turn allowed the proofs to successfully check. But adding the {C} even 
without --proof-irrelevance results in the significantly improved memory/stack 
usage.

I suppose the fact that the proofs in question use all of the operations from 
the _Product module many times explains why they had such an impact. Still, 
it's a bit of a surprise that filling that implicit argument in causes such a 
vast difference in performance. I guess without specifying it, the module may 
get opened still parameterized by C, and the category record may be getting 
eta expanded and re-evaluated dozens of times, since it needs to be passed to 
almost every individual term in the proof? I'm a bit confused as to why I get 
complaints with Prop equality (and proof irrelevance; I haven't bothered with 
a lot of experimentation about which situations exactly cause it to turn 
yellow), but not with Set equality, though.

Anyhow, thanks for your help.

-- Dan