[Agda] Associativity for free!
Alan Jeffrey
ajeffrey at bell-labs.com
Wed Oct 26 16:48:55 CEST 2011
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.
More information about the Agda
mailing list