[Agda] type check cost for `open'

[Peter Selinger]

Hi all,

I'm in the process of formalizing a moderately large project in Agda,
and I would like to echo the experience of Sergei and others:
reduction performance is a major bottleneck - perhaps the greatest
issue standing in the way of making Agda truly useable. 

I've been doctoring around with symptoms: introducing a bit of
strictness here and there, splitting modules, etc. These workarounds
are ugly, never quite solve the problem completely, and sometimes they
introduce additional complications and proof obligations.

What would it take to equip Agda with an efficient evaluation
strategy? For example, would this be as simple as providing an
alternate implementation of a handful of modules in the Agda source
code? Or is it something that would require deeper modifications
throughout the system?

Here is an example I was struggling with and just worked out. 
I am dealing with word problems in monoids, and I have written a
function comm-canonical that inputs a word and outputs a canonical
form modulo commutativity of generators. The implementation is
correct, but I'm not concerned with correctness at the moment; only
with the running time.

The 4 functions defined in the module Commuting should in principle be
efficient. All of the functions are linear (in the sense that each
argument is used exactly once), so there should be no special issues
related to evaluation strategy. In principle, the functions split,
unsplit, and insert should run in time O(n), and comm-canonical should
run in time O(n^2), where n is the length of the list.

-- ----------------------------------------------------------------------
-- BEGIN CODE
-- ----------------------------------------------------------------------

open import Data.Bool
open import Data.Nat
open import Data.List
open import Data.Product

module CommTest where

-- ----------------------------------------------------------------------
-- General-purpose stuff

-- Prepend the reverse of the first list to the second one.
reverse-prepend : ∀ {X : Set} -> List X -> List X -> List X
reverse-prepend [] ys = ys
reverse-prepend (x ∷ xs) ys = reverse-prepend xs (x ∷ ys)

-- ----------------------------------------------------------------------
-- Module Commuting: given a set X, a commutativity relation on X, and
-- an ordering on X, compute a canonical form of words in X, modulo
-- commutativity.
module Commuting
  (X : Set)
  (comm : X -> X -> Bool)
  (less : X -> X -> Bool)
  where

  -- Given ys, x, and zs, return (revert zs1 @ ys , zs2), where zs =
  -- zs1 @ zs2 and zs1 is the longest prefix of zs all of whose
  -- elements commute with x.
  split : List X -> X -> List X -> List X × List X
  split ys x [] = (ys , [])
  split ys x (z ∷ zs) with comm x z
  split ys x (z ∷ zs) | false = (ys , (z ∷ zs))
  split ys x (z ∷ zs) | true = split (z ∷ ys) x zs
  
  -- Given ys, x, and zs, return revert ys' @ zs, where ys' is the
  -- lexicographically smallest word that can be obtained by inserting
  -- x in ys. We assume that revert ys @ zs is a canonical form.
  unsplit : List X -> X -> List X -> List X
  unsplit [] x zs = x ∷ zs
  unsplit (y ∷ ys) x zs with less x y
  unsplit (y ∷ ys) x zs | false = unsplit ys x (y ∷ zs)
  unsplit (y ∷ ys) x zs | true = reverse-prepend (y ∷ ys) (x ∷ zs)
  
  -- Given x and xs, where xs is already a canonical form, return the
  -- canonical form of x ∷ xs.
  insert : X -> List X -> List X
  insert x xs =
    let (ys , zs) = split [] x xs
    in
      unsplit ys x zs
  
  -- Return the canonical form of a word, modulo commutativity of
  -- generators.  Of all equivalent words, the canonical form is the
  -- least one in the reverse lexicographic order.
  comm-canonical : List X -> List X
  comm-canonical [] = []
  comm-canonical (x ∷ xs) = insert x (comm-canonical xs)

-- ----------------------------------------------------------------------
-- A trivial example use of Commuting.

data Gen : Set where
  A : Gen

my-comm : (x y : Gen) -> Bool
my-comm A A = true

my-less : Gen -> Gen -> Bool
my-less A A = false

open module Commuting-Gen = Commuting Gen my-comm my-less

test : ℕ -> List Gen
test n = comm-canonical (replicate n A)

-- ----------------------------------------------------------------------
-- END CODE
-- ----------------------------------------------------------------------

However, testing shows that evaluating the function "test" takes
exponential time:

test 16: 7 seconds
test 17: 15 seconds
test 18: 30 seconds
test 19: 60 seconds

etc.

After much investigation (and befuddlement), I realized the source of
the problem, which is actually the fact that the function split
returns a pair. Because of Agda's normal order evaluation without
sharing, the expression

let (ys , zs) = bla

is actually translated to

let ys = fst bla
    zs = snd bla,

which means that bla is evaluated twice. The only possible workaround
(that I was able to find) was to translate split into continuation
passing style:

  split : ∀ {K : Set} -> List X -> X -> List X -> (List X -> List X -> K) -> K
  split ys x [] k = k ys []
  split ys x (z ∷ zs) k with comm x z
  split ys x (z ∷ zs) k | false = k ys (z ∷ zs)
  split ys x (z ∷ zs) k | true = split (z ∷ ys) x zs k
  
  insert : X -> List X -> List X
  insert x xs =
    split [] x xs (λ ys zs -> unsplit ys x zs)

And voila, now the evaluation is lightning fast (and no longer
exponential)!

However, CPS style is not my favorite way of programming; it is
something that should be done internally within a programming
language, and not by the programmer.

I suspect that where Sergei and others have reported evaluation times
of 1-2 hours or longer, similar forces may be at work. If Agda could
be equipped with a proper lazy evaluation strategy, I think it would
solve a lot of these problems. I'd be happy to chip in if there's a
way to do this.

Thanks, -- Peter