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

≡-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.

_______________________________________________

Agda mailing list