[Agda] Re: Associativity for free!

[Alan Jeffrey]

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.