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