<div><div>Hi Alan,</div><div><br></div><div>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.</div><div><br></div><div>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:</div><div><br></div><div> .ok : {x : List A} → (fun x ≡ (list ++ x))</div><div><div><br></div><div>Solves this problem (and doesn't break anything, as far as I can tell). Perhaps I am missing something obvious?</div><div><br></div><div>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.</div><div><br></div><div>Cheers, this looks really cool!</div><br>Liam O'Connor</div></div>
<p style="color: #A0A0A8;">On Thursday, 27 October 2011 at 1:48 AM, Alan Jeffrey wrote:</p>
<blockquote type="cite" style="border-left-style:solid;border-width:1px;margin-left:0px;padding-left:10px;">
<span><div><div><div>Hi everyone,</div><div><br></div><div>A quick note about a trick for representing lists (or any other monoid) </div><div>up to associativity. Am I reinventing a wheel here?</div><div><br></div><div>I've been doing some mucking around recently with proofs about </div><div>lambda-calculi and was hitting annoying problems with associativity</div><div>on lists. A prototypical example is:</div><div><br></div><div> weakening : ∀ {A a} (as bs cs : List A) →</div><div> (a ∈ (as ++ cs)) → (a ∈ (as ++ bs ++ cs))</div><div><br></div><div>It's easy to prove that ++ is associative, but making use of that fact </div><div>is rather painful, as there's lots of manual wiring with subst and cong, </div><div>for example:</div><div><br></div><div> weaken2 : ∀ {A a} (as bs cs ds : List A) →</div><div> (a ∈ (as ++ bs ++ ds)) → (a ∈ (as ++ bs ++ cs ++ ds))</div><div> weaken2 {A} {a} as bs cs ds a∈es =</div><div> subst (λ X → (a ∈ X)) (++-assoc as bs (cs ++ ds))</div><div> (weakening (as ++ bs) cs ds</div><div> (subst (λ X → (a ∈ X)) (sym (++-assoc as bs ds)) a∈es))</div><div><br></div><div>This gets tiresome pretty rapidly. Oh if only there were a data </div><div>structure which represented lists, but for which ++ was associative up </div><div>to beta reduction... Oh look there already is one, it's called </div><div>difference lists. Quoting the standard library:</div><div><br></div><div> DiffList : Set → Set</div><div> DiffList a = List a → List a</div><div><br></div><div> _++_ : ∀ {a} → DiffList a → DiffList a → DiffList a</div><div> xs ++ ys = λ k → xs (ys k)</div><div><br></div><div>Unfortunately, difference lists are not isomorphic to lists: there's a </div><div>lot more functions on lists than just concatenation functions. This </div><div>causes headaches (e.g. writing inductive functions on difference lists).</div><div><br></div><div>A first shot at fixing this is to write a data structure for those </div><div>difference lists which are concatenations:</div><div><br></div><div> record Seq (A : Set) : Set where</div><div> constructor seq</div><div> field</div><div> list : List A</div><div> fun : List A → List A</div><div> ok : fun ≡ _++_ list -- Broken</div><div><br></div><div>It's pretty straightforward to define the monoidal structure for Seq:</div><div><br></div><div> ε : ∀ {A} → Seq A</div><div> ε = seq [] id refl</div><div><br></div><div> _+_ : ∀ {A} → Seq A → Seq A → Seq A</div><div> (seq as f f✓) + (seq bs g g✓) = seq (f bs) (f ∘ g) (...easy lemma...)</div><div><br></div><div>Unfortunately, we're back to square one again, because + is only </div><div>associative up to propositional equality, not beta reduction. This time, </div><div>it's the ok field that gets in the way. So we can fix that, and just </div><div>make the ok field irrelevant, that is:</div><div><br></div><div> record Seq (A : Set) : Set where</div><div> constructor seq</div><div> field</div><div> list : List A</div><div> fun : List A → List A</div><div> .ok : fun ≡ _++_ list -- Fixed</div><div><br></div><div> open Seq public renaming (list to [_])</div><div><br></div><div>Hooray, + is now associative up to beta reduction:</div><div><br></div><div> +-assoc : ∀ {A} (as bs cs : Seq A) →</div><div> ((as + bs) + cs) ≡ (as + (bs + cs))</div><div> +-assoc as bs cs = refl</div><div><br></div><div>Moreover, given (<a href="http://thread.gmane.org/gmane.comp.lang.agda/3034">http://thread.gmane.org/gmane.comp.lang.agda/3034</a>):</div><div><br></div><div> ≡-relevant : ∀ {A : Set} {a b : A} → .(a ≡ b) → (a ≡ b)</div><div><br></div><div>we can define:</div><div><br></div><div> data Case {A : Set} : Seq A → Set where</div><div> [] : Case ε</div><div> _∷_ : ∀ a as → Case (a ◁ as)</div><div><br></div><div> case : ∀ {A} (as : Seq A) → Case as</div><div><br></div><div>and this gives us recursive functions over Seq (which somewhat to my </div><div>surprise actually get past the termination checker), for example:</div><div><br></div><div> ids : ∀ {A} → Seq A → Seq A</div><div> ids as with case as</div><div> ids .(a ◁ as) | a ∷ as = a ◁ ids as</div><div> ids .ε | [] = ε</div><div><br></div><div>For example, we can now define weakening:</div><div><br></div><div> weakening : ∀ {A a} (as bs cs : Seq A) →</div><div> (a ∈ [ as + cs ]) → (a ∈ [ as + bs + cs ])</div><div><br></div><div>and use it up to associativity without worrying hand-coded wiring:</div><div><br></div><div> weaken2 : ∀ {A a} (as bs cs ds : Seq A) →</div><div> (a ∈ [ as + bs + ds ]) → (a ∈ [ as + bs + cs + ds ])</div><div> weaken2 as bs = weakening (as + bs)</div><div><br></div><div>Hooray, cake! Eating it!</div><div><br></div><div>I suspect this trick works for most any monoid, so you can do </div><div>associativity on naturals, vectors, partial orders with join, etc. etc.</div><div><br></div><div>The idea of using difference lists to represent lists is standard, but </div><div>as far as I know, this use of irrelevant equalities to get structural </div><div>recursion is new. Anyone know of any prior art?</div><div><br></div><div>A.</div><div>_______________________________________________</div><div>Agda mailing list</div><div><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a></div><div><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></div></div></div></span>
</blockquote>
<div>
<br>
</div>