[Agda] Associativity for free!

[Alan Jeffrey]

Hi everyone,

A quick note about a trick for representing lists (or any other monoid) 
up to associativity. Am I reinventing a wheel here?

I've been doing some mucking around recently with proofs about 
lambda-calculi and was hitting annoying problems with associativity
on lists. A prototypical example is:

   weakening : ∀ {A a} (as bs cs : List A) →
    (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))

It's easy to prove that ++ is associative, but making use of that fact 
is rather painful, as there's lots of manual wiring with subst and cong, 
for example:

   weaken2 : ∀ {A a} (as bs cs ds : List A) →
     (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))
   weaken2 {A} {a} as bs cs ds a∈es =
     subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))
       (weakening (as ++ bs) cs ds
         (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))

This gets tiresome pretty rapidly. Oh if only there were a data 
structure which represented lists, but for which ++ was associative up 
to beta reduction... Oh look there already is one, it's called 
difference lists. Quoting the standard library:

   DiffList : Set → Set
   DiffList a = List a → List a

   _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a
   xs ++ ys = λ k → xs (ys k)

Unfortunately, difference lists are not isomorphic to lists: there's a 
lot more functions on lists than just concatenation functions. This 
causes headaches (e.g. writing inductive functions on difference lists).

A first shot at fixing this is to write a data structure for those 
difference lists which are concatenations:

   record Seq (A : Set) : Set where
     constructor seq
     field
       list : List A
       fun : List A → List A
       ok : fun ≡ _++_ list  -- Broken

It's pretty straightforward to define the monoidal structure for Seq:

   ε : ∀ {A} → Seq A
   ε = seq [] id refl

    _+_ : ∀ {A} → Seq A → Seq A → Seq A
   (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)

Unfortunately, we're back to square one again, because + is only 
associative up to propositional equality, not beta reduction. This time, 
it's the ok field that gets in the way. So we can fix that, and just 
make the ok field irrelevant, that is:

   record Seq (A : Set) : Set where
     constructor seq
     field
       list : List A
       fun : List A → List A
       .ok : fun ≡ _++_ list  -- Fixed

   open Seq public renaming (list to [_])

Hooray, + is now associative up to beta reduction:

   +-assoc : ∀ {A} (as bs cs : Seq A) →
     ((as + bs) + cs) ≡ (as + (bs + cs))
   +-assoc as bs cs = refl

Moreover, given (http://thread.gmane.org/gmane.comp.lang.agda/3034):

   ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)

we can define:

   data Case {A : Set} : Seq A → Set where
     [] : Case ε
     _∷_ : ∀ a as → Case (a ◁ as)

   case : ∀ {A} (as : Seq A) → Case as

and this gives us recursive functions over Seq (which somewhat to my 
surprise actually get past the termination checker), for example:

   ids : ∀ {A} → Seq A → Seq A
   ids as        with case as
   ids .(a ◁ as) | a ∷ as = a ◁ ids as
   ids .ε        | []     = ε

For example, we can now define weakening:

   weakening : ∀ {A a} (as bs cs : Seq A) →
     (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])

and use it up to associativity without worrying hand-coded wiring:

   weaken2 : ∀ {A a} (as bs cs ds : Seq A) →
     (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])
   weaken2 as bs = weakening (as + bs)

Hooray, cake! Eating it!

I suspect this trick works for most any monoid, so you can do 
associativity on naturals, vectors, partial orders with join, etc. etc.

The idea of using difference lists to represent lists is standard, but 
as far as I know, this use of irrelevant equalities to get structural 
recursion is new. Anyone know of any prior art?

A.