[Agda] heap mistery

[Martin Escardo]

This is hopefully for the benefit of those of you who run into heap
problems with code that should theoretically work, and would like to
find a workaround.

Summary: Uses of general dependently-typed destructors/eliminators
appear to be way more memory-hungry during compilation than particular
instances expressed directly by pattern matching.

On 19/05/11 18:03, Andreas Abel wrote:
> thanks for the bug report. If you have time, could you put it on

I did, and Andreas kindly looked at it, and we both thought about it
in detail today, and performed some (complementary) experiments and
saw some traces. The conclusion of Andreas', with which I agree, is
that this seems to be an issue with the unification engine.

Theoretically speaking, it is not a bug: there are no loops, just huge
terms. (This was done with code with termination checking enabled in
all modules.)

I gave an example of rewriting of the code that avoids the heap
problem in the original message I sent to the list.  I discuss it
briefly here. Recall:

>> I prove an existential Theorem, and then define
>>
>> program₂ : ₂ℕ → (m : ℕ) → (smaller(m + 1) → ℕ)
>> program₂ α m = ∃-witness(∃-elim (Theorem α m))
>>
>> This makes Agda compilation run for some time until the heap is
>> exhausted.
>>
>> Now I instead define the two programs by pattern matching rather than
>> the destructors ∃-witness and ∃-elim (first and second projection):
>>
>> program₂ : ₂ℕ → (m : ℕ) → (smaller(m + 1) → ℕ)
>> program₂ α m = f(Theorem α m)
>> where
>>   f : Finite-Pigeonhole α m → (smaller(m + 1) → ℕ)
>>   f(∃-intro b (∃-intro s proof)) = s -- f is ∃-witness o ∃-elim!!!
>>
>>  Compilation is instanteneous and succeeds using neglegible memory.

As a term, yes, f is that! But the type of the pattern "proof" is not
computed in this definition. However, using ∃-witness(∃-elim ...)), it
is computed, and it is huge:

>> data ∃ {X : Set} (A : X → Ω) : Ω where
>>  ∃-intro : (x₀ : X) → A x₀ → ∃ \(x : X) → A x
>>
>> ∃-witness : {X : Set} {A : X → Ω} → (∃ \(x : X) → A x) → X
>> ∃-witness (∃-intro x a) = x
>>
>> ∃-elim : {X : Set} {A : X → Ω} →
>>  (proof : ∃ \(x : X) → A x) → A (∃-witness proof)
>> ∃-elim (∃-intro x a) = a

The moral, I think, is that dependent destruction as in ∃-elim is more
expensive that pattern matching. It is not the definition of the term
∃-elim that is causing the size explosion problem, but the definition
of its type. Which is of course needed for ∃-elim, but not for
program2.

I have seen, but not paid attention to, discussions in this list about
heap-exhaustion problems. I wonder whether they can be solved in an
analogous manner. Anyway, I have learned something useful - thanks
Andreas!

Sorry to sound critical of the work on Agda: I am not. Apart from
these minor glitches, I really like Agda: it is (syntactically and
mathematically) elegant, relatively efficient, user friendly, and a
pleasure to work with. It is the nicest practical manifestation of
functional programming with specifications and correctness proofs
naturally built-in in the language and embedded into programs. I plan
to teach this to undergrads in the near future, and a number of my
colleagues support this idea. Thanks to Ulf Norell and the other
people, before and after him, who made this possible!  You've made an
important (and fun) contribution.

Best wishes,
Martin