[Agda] Re: Associativity for free!

[Andrea Vezzosi]

By the way you get to write both weakening and substitution as special
cases of the bind operator for the right monad:

https://github.com/Saizan/agda-frp-js/commit/07bd98c30a8669d2c5dd3d69aa4a12bf566c7ae0

(and then i proved a bunch of not so relevant stuff in the middle)

-- Andrea

On Wed, Nov 2, 2011 at 10:10 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
> I'll have a look at it, thanks for the pointer!
>
> I'm going to be needing the general form of substitution later (in stuff
> I've not committed yet, which does normalization by evaluation). That's not
> to say I couldn't derive the general form from substitution and weakening,
> but I think it's swings and roundabouts.
>
> A.
>
> On 11/02/2011 12:46 PM, Andreas Abel wrote:
>>
>> Hi Alan,
>>
>> you might be interested in a trick how to fuse weakening and
>> substitution into a single operation.  I have done this for
>> non-wellscoped de Bruijn terms in Agda:
>>
>>    http://www2.tcs.ifi.lmu.de/~abel/ParallelSubstitution.agda
>>
>> but Thorsten and Conor deserve the credit for it (pointers in the .agda
>> file).
>>
>> Looking at your code I wonder whether substitution (substn+) could not
>> be a bit less general, since N remains in the same context always.
>> Usually I prove the substitution lemma like this:
>>
>>    Gamma, x : T, Delta |- M : U
>>    Gamma               |- N : T
>>    ----------------------------
>>    Gamma, Delta   |- M[N/x] : U
>>
>> Your statement has a more general context form for N, but I wonder
>> whether this is necessary.
>>
>> Cheers,
>> Andreas
>>
>> On 11/2/11 5:26 PM, Alan Jeffrey 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
>>>
>>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>