[Agda] Agda performance improvements

[Martin Escardo]

Great. I see that the example I reported a while ago producing a heap 
exhaustion now type-checks, as tested by you, and fast. Many thanks, 
Ulf! Martin

On 25/08/11 14:40, Ulf Norell wrote:
> Hi folks,
>
> I have improved how Agda handles record projections by not keeping the
> record parameters as
> arguments internally. For the user there is no difference except that
> some programs will type check
> <unbounded> times faster. The standard library checks 30% faster and
> requires 30% less memory
> to give you an idea of what to expect.
>
> Here's an example which couldn't be type checked before (on present day
> computers):
>
>
>     {-# OPTIONS --type-in-type #-}  -- just so I don't have bother with
>     universe polymorphism
>     module Cat where
>
>     infixr 2 _,_
>     record Σ (A : Set)(B : A → Set) : Set where
>        constructor _,_
>        field fst : A
>              snd : B fst
>
>     open Σ
>
>     data ⊤ : Set where
>        tt : ⊤
>
>     ∃ : {A : Set}(B : A → Set) → Set
>     ∃ B = Σ _ B
>
>     infix 10 _≡_
>
>     data _≡_ {A : Set}(a : A) : A → Set where
>        refl : a ≡ a
>
>     Cat : Set
>     Cat =
>        ∃ λ (Obj : Set) →
>        ∃ λ (Hom : Obj → Obj → Set) →
>        ∃ λ (id : ∀ X → Hom X X) →
>        ∃ λ (_○_ : ∀ {X Y Z} → Hom Y Z → Hom X Y → Hom X Z) →
>        ∃ λ (idl : ∀ {X Y}{f : Hom X Y} → id Y ○ f ≡ f) →
>        ∃ λ (idr : ∀ {X Y}{f : Hom X Y} → f ○ id X ≡ f) →
>        ∃ λ (assoc : ∀ {W X Y Z}{f : Hom W X}{g : Hom X Y}{h : Hom Y Z} →
>                      (h ○ g) ○ f ≡ h ○ (g ○ f)) →
>        ⊤
>
>     Obj : (C : Cat) → Set
>     Obj C = fst C
>
>     Hom : (C : Cat) → Obj C → Obj C → Set
>     Hom C = fst (snd C)
>
>     id : (C : Cat) → ∀ X → Hom C X X
>     id C = fst (snd (snd C))
>
>     comp : (C : Cat) → ∀ {X Y Z} → Hom C Y Z → Hom C X Y → Hom C X Z
>     comp C = fst (snd (snd (snd C)))
>
>     idl : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C (id C Y) f ≡ f
>     idl C = fst (snd (snd (snd (snd C))))
>
>     idr : (C : Cat) → ∀ {X Y}{f : Hom C X Y} → comp C f (id C X) ≡ f
>     idr C = fst (snd (snd (snd (snd (snd C)))))
>
>     assoc : (C : Cat) → ∀ {W X Y Z}{f : Hom C W X}{g : Hom C X Y}{h :
>     Hom C Y Z} →
>              comp C (comp C h g) f ≡ comp C h (comp C g f)
>     assoc C = fst (snd (snd (snd (snd (snd (snd C))))))
>
>
> The implicit A and B arguments to fst and snd (whose types are
>    fst : {A : Set}{B : A → Set} → Σ A B → A
>    snd : {A : Set}{B : A → Set} (p : Σ A B) → B (fst p)
> ) make this explode. With the new optimisation the example checks in
> half a second.
>
> Incidentally, Coq seem to suffer from the same problem, or so I'm told
> by people who tried
> to implement the example in Coq.
>
> / Ulf
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe