[Agda] Re: Associativity for free!

[Andreas Abel]

Thanks!

That extra comes with your revised definition of difference lists. 
Sounds good!

Is it that the irrelevant proofs show up in the error messages always? 
Maybe it would be helpful to be able to switch of printing of irrelevant 
terms?

Cheers,
Andreas

On 3/22/12 3:47 PM, Alan Jeffrey wrote:
> The version that's up on github does both left- and right-units as well
> as associativity. The canonical example is difference naturals:
>
>
> https://github.com/agda/agda-assoc-free/blob/master/src/AssocFree/DNat.agda
>
> which includes:
>
> -- Addition forms a monoid on the nose
>
> +-assoc : ∀ l m n → (((l + m) + n) ≡ (l + (m + n)))
> +-assoc l m n = refl
>
> +-unit₁ : ∀ n → ((♯0 + n) ≡ n)
> +-unit₁ n = refl
>
> +-unit₂ : ∀ n → ((n + ♯0) ≡ n)
> +-unit₂ n = refl
>
> Don't forget what I said about incomprehensible and huge normal forms
> getting in the way of debugging!
>
> A.
>
> On 03/22/2012 09:40 AM, Andreas Abel wrote:
>> 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/