⋆ Talk/discussion: Some tricks for making Agda code faster

Nils Anders Danielsson

⋆ Rules of thumb

Some rules of thumb for making Agda code type-check faster:

* If things start to become slow, don't buy a faster machine, change
  the code.

* Try to avoid making Agda compare large terms.

⋆ Avoid making Agda compare large terms

How can one avoid making Agda compare large terms?

⋆⋆ Abstract

One option is to use abstract. This can work well for terms that are,
in some sense, irrelevant. Example: Equality proofs in the presence of
UIP.

⋆⋆ Prevent unfolding

Another method is to make sure that terms are not unfolded until you
"ask for it".

⋆⋆⋆ Patterns

Pattern matching blocks evaluation until the defined thing is applied
to something with enough constructors.

But not for records with η-equality.

If there is nothing to match on, then one can add an extra argument of
type Unit (for a unit type without η-equality).

⋆⋆⋆ Copatterns

Definitions using copatterns block evaluation until enough copatterns
have been applied to the defined thing.

Also for records with η-equality.

Note that Agda automatically converts certain definitions of the form

  lhs = record { … record { … } … }

into definitions that use copatterns. I am not sure exactly what the
criteria are, but the record types have to have η-equality enabled.

⋆ Some examples from code that I have worked on recently

⋆⋆ Quotient

I wanted to define one eliminator, and then a bunch of other
eliminators in terms of the first one. However, this led to
performance problems, so I used explicit pattern matching for two of
the other eliminators.

⋆⋆⋆ Fix 1

Bundle eliminator arguments using record types, use copatterns to
define the bundles.

This fixed some problems, but not all.

⋆⋆⋆ Fix 2

Turn off η-equality for the record types.

With η-equality for the record types I would hope that you get exactly
the same definitional equalities as when the eliminators are defined
in curried form. However, in some cases Agda might η-expand a term.

⋆⋆ Lens.Non-dependent.Higher

Problems when checking that an already defined composition law
("id ∘ l ≡ l") had the right type.

In this case Agda should not care about how the law is defined, it
should only check that the types match. Thus one might suspect that
the definitions of identity and composition are problematic.

⋆⋆⋆ Non-fix 1

Defining composition using copatterns.

Perhaps Agda decided to η-expand something.

⋆⋆⋆ Non-fix 2

Turning off η-equality, defining composition using copatterns.

I made use of an η-rule in the code, and I don't think you can prove
the η-rule without pattern matching. (And even if this law is
postulated, and the second fix below is applied, Agda is for some
reason still slow.)

UPDATE: Thorsten Altenkirch and Andrea Vezzosi mentioned during the
talk that you can prove this kind of η-rule using Cubical Agda.

⋆⋆⋆ Fix 1

Turning off η-equality, turning off copatterns, defining composition
using pattern matching:

  record Lens (A : Set a) (B : Set b) : Set (lsuc (a ⊔ b)) where
    constructor ⟨_,_,_⟩
    pattern
    no-eta-equality
    ⋮

  … l₁@(⟨ _ , _ , _ ⟩) l₂@(⟨ _ , _ , _ ⟩) = record …

This fixed the problems mentioned above, but I encountered further
problems related to an identity lens id, and one cannot define id
using matching on some input lens.

⋆⋆⋆ Fix 2

Adding an artificial argument to id:

  id : Block "id" → Lens A A
  id {A = A} ⊠ = record …

Here "Block s" stands for a unit type without η-equality:

  Block : String → Set
  Block _ = Unit

  pattern ⊠ = unit

This fixed more problems. However, I find it rather annoying to pass
around values of type Unit.

⋆⋆⋆ Combinators for working with Block

The following eliminator is perhaps not very interesting:

  unblock : (b : Unit) (P : Unit → Set p) → P ⊠ → P b
  unblock ⊠ _ p = p

However, the following combinator can be useful:

  block : (Unit → A) → A
  block f = f ⊠

Here is one example of its use:

  category :
    Block "category" →
    Univalence a →
    Category (lsuc a) (lsuc a)
  category ⊠ univ =
    block λ b →
    C.precategory-with-SET-to-category
      ext
      (λ _ _ → univ)
      (proj₂ $ precategory′ b univ)
      (λ (_ , A-set) _ → ≃≃≅ b univ A-set)
      (λ (_ , A-set) → ≃≃≅-id≡id b univ A-set)

The definition of the category does not unfold automatically, due to
the ⊠ pattern. However, inside the definition there are three parts
that should match up. If "b" is replaced by "⊠", then the code
type-checks slower. One option would be to let category take two
"Block" arguments, but that sounds rather annoying to me. An
alternative is to block locally using the block combinator.

⋆ Emacs setup

Local variables:
outline-regexp: "⋆+"
End: