[Agda] Re: Associativity for free!

[Andreas Abel]

Hi Alan,

I remembered your idea when working with Frederic Kettelhoit on an 
implementation of Fingertrees which are parametrized by a monoid.

You trick gives associativity for free.  Then, left-unit is already for 
free.  Is there a way to also get the right-unit for free?

Cheers,
Andreas

On 11/21/11 8:17 PM, Alan Jeffrey wrote:
> I've now finished up the NBE algorithm for the simply-typed
> lambda-calculus. It defines a reduction semantics, and uses NBE to show
> that every term reduces to one in normal form.
>
> At this point, I'm afraid I think of this as an interesting idea, but
> one where some pragmatic nastiness gets in the way of it being useful.
> The main problems are:
>
> - Huge normal forms, which slow Agda down horribly.
>
> - Incomprehensible normal forms, which make debugging remarkably difficult.
>
> - Less unification -- from unifying (a :: as) with (b :: bs) Agda
> doesn't unify a with b or as with bs.
>
> The implementation is up at https://github.com/agda/agda-assoc-free
>
> A.
>
> On 11/02/2011 11:26 AM, Jeffrey, Alan S A (Alan) wrote:
>> Hi everyone,
>>
>> My original motivation for "associativity for free" was properties about
>> lambda-calculi. I've now worked through some of the details, and here is
>> the syntax of the simply-typed lambda-calculus:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda
>>>
>>
>> The interesting thing is weakening, with type:
>>
>> weaken+ : ∀ B Γ Δ {T} → Exp (B ++ Δ) T → Exp (B ++ Γ ++ Δ) T
>>
>> and (news just in!) weakening commutes with itself (up to propositional
>> equality):
>>
>> weaken+ Φ Ψ (B ++ Γ ++ Δ) (weaken+ (Φ ++ B) Γ Δ M)
>> ≡ weaken+ (Φ ++ Ψ ++ B) Γ Δ (weaken+ Φ Ψ (B ++ Δ) M)
>>
>> Note that you can't even state this property without associativity on
>> the nose, since the lhs has type (Φ ++ Ψ ++ (B ++ Γ ++ Δ)) and the rhs
>> has type ((Φ ++ Ψ ++ B) ++ Γ ++ Δ).
>>
>> The proof makes use of a list-membership type, defined in:
>>
>>> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/DList.agda
>>>
>>
>> It satisfies weakening on the left and right:
>>
>> _≪_ : ∀ {A a as} → (a ∈ as) → ∀ bs → (a ∈ (as ++ bs))
>> _≫_ : ∀ {A a bs} → ∀ as → (a ∈ bs) → (a ∈ (as ++ bs))
>>
>> and moreover has left and right units and associativity properties, all
>> up to beta-equivalence (that is, all these properties have proof refl):
>>
>> (a∈as ≪ []) ≡ a∈as
>> ([] ≫ a∈as) ≡ a∈as
>> (a∈as ≪ bs ≪ cs) ≡ (a∈as ≪ bs ++ cs)
>> ((as ≫ a∈bs) ≪ cs) ≡ (as ≫ (a∈bs ≪ cs))
>> (as ≫ bs ≫ a∈cs) ≡ (as ≫ bs ≫ a∈cs)
>>
>> Under the hood, this is implemented in terms of difference naturals
>> (that is an implementation of ℕ where + and ♯0 form a monoid up to
>> beta-equivalence), and an implementation of difference lists such that
>> the length function is a monoid homomorphism up to beta-equivalence:
>>
>> (len (as ++ bs) ≡ (len as + len bs))
>> (len [] ≡ ♯0)
>>
>> With all that in place, the proof of weakening is pretty
>> straightforward. The only case which requires any work is variables, and
>> a typical case is:
>>
>> begin
>> xweaken+ Φ Ψ (B ++ Γ ++ Δ) (case Φ (B ++ Γ ++ Δ) (Φ ≫ x ≪ Γ ≪ Δ))
>> ≡⟨ cong (xweaken+ Φ Ψ (B ++ Γ ++ Δ)) (case-≫ Φ (x ≪ Γ ≪ Δ)) ⟩
>> (Φ ≫ Ψ ≫ x ≪ Γ ≪ Δ)
>> ≡⟨ cong (xweaken+ (Φ ++ Ψ ++ B) Γ Δ) (sym (case-≪ (Φ ≫ Ψ ≫ x) Δ)) ⟩
>> xweaken+ (Φ ++ Ψ ++ B) Γ Δ (case (Φ ++ Ψ ++ B) Δ (Φ ≫ Ψ ≫ x ≪ Δ))
>> ∎
>>
>> I don't really want to think about what this proof would look like with
>> all the associativity wiring made explicit.
>>
>> There is still a bit of annoying associativity left, because I can't see
>> how to get coproducts to associate on the nose, so there's lots of gore
>> needed to define a case function:
>>
>> data Case {A} a (as bs : List A) : Set where
>> inj₁ : (a∈as : a ∈ as) → Case a as bs
>> inj₂ : (a∈bs : a ∈ bs) → Case a as bs
>>
>> case : ∀ {A a} as bs → (a ∈ (as ++ bs)) → Case {A} a as bs
>>
>> and then prove that it satisfies associativity (up to propositional
>> equality, not beta-equivalence).
>>
>> A.
>>
>> On 10/26/2011 09:48 AM, Jeffrey, Alan S A (Alan) 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
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/