[Agda] Associativity for free!

[Liam O'Connor]

Hi Alan,

I'm not aware of any prior art, but this is really nice. A few questions, based on my attempt to repeat your work. I'm a bit of a novice in Agda, so bear with me.

1. I couldn't use your definitions as-is without postulating extensional equality (i.e point wise equality = propositional functional equality) . Rephrasing your ok type as follows:

    .ok : {x : List A} → (fun x ≡ (list ++ x))

Solves this problem (and doesn't break anything, as far as I can tell). Perhaps I am missing something obvious?

2. I could not come up with a satisfactory way to define your "case" function, even with =-relevant. Care to share your implementation? Once again, I could just be being thick.

Cheers, this looks really cool!
Liam O'Connor  

On Thursday, 27 October 2011 at 1:48 AM, Alan Jeffrey wrote:

> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se (mailto:Agda at lists.chalmers.se)
> https://lists.chalmers.se/mailman/listinfo/agda
>  
>  


-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20111027/619c6caa/attachment-0001.html