[Agda] Re: Associativity for free!

[Alan Jeffrey]

Switching off printing irrelevant arguments would certainly help with 
debugging. The terms will still be huge, so Agda may be sloooowwww.

A.

On 03/22/2012 11:22 AM, Andreas Abel wrote:
> 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
>>>>
>>>
>>
>