[Agda] Agda performance improvements
Ulf Norell
ulfn at chalmers.se
Thu Aug 25 15:40:03 CEST 2011
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110825/a96782b1/attachment.html
More information about the Agda
mailing list