Alan Jeffrey | 26 Oct 16:48 2011

Associativity for free!

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
(Continue reading)

Liam O'Connor | 26 Oct 19:32 2011
Picon
Picon

Re: Associativity for free!

Hi Alan,

I'm not aware of any prior art, but this is really nice. A few questions, based on my attempt to repeat your work. I'm a bit of a novice in Agda, so bear with me.

1. I couldn't use your definitions as-is without postulating extensional equality (i.e point wise equality = propositional functional equality) . Rephrasing your ok type as follows:

    .ok : {x : List A} → (fun x ≡ (list ++ x))

Solves this problem (and doesn't break anything, as far as I can tell). Perhaps I am missing something obvious?

2. I could not come up with a satisfactory way to define your "case" function, even with =-relevant. Care to share your implementation? Once again, I could just be being thick.

Cheers, this looks really cool!

Liam O'Connor

On Thursday, 27 October 2011 at 1:48 AM, Alan Jeffrey 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


≡-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 mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
James Chapman | 26 Oct 23:01 2011
Picon
Picon

Re: Associativity for free!

Hi Alan, 

I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.

1. A trivial solution for your example is simply to make _++_ associate to the left:

data List (X : Set) : Set where
 []   : List X
 _::_ : X → List X → List X

_++_ : ∀{X} → List X → List X → List X
[]        ++ xs' = xs'
(x :: xs) ++ xs' = x :: (xs ++ xs')

infixl 5 _++_

postulate P : ∀{X} → List X → Set

postulate weakening : ∀ {A} (as bs cs : List A) →
                      P (as ++ cs) → P (as ++ bs ++ cs)

weaken2 : ∀ {A} (as bs cs ds : List A) →
   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p

This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse told
me that in a recent implementation of a dependently typed lambda calculus he defined both versions and
didn't end up needing them both at the same time. Do you need both at the same time?

2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I learnt
from Conor (exercise 15, his AFP notes http://www.strictlypositive.org/epigram-notes.ps.gz) is
simply to avoid it. Instead of giving weakening this type, give a first order presentation of weakenings
(functions from a context to the same context with more stuff chucked in arbitrary places). For  lists this
function space would be the following inductively defined sublist relation:

data _≤_ {X : Set} : List X → List X → Set where
  done : [] ≤ []
  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')

Then, weakening would be something like:

weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'

By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called order
preserving embeddings) in chapter 4 of my thesis (http://www.cs.ioc.ee/~james/papers/thesis.pdf )
and it was much more pleasant than using ++ as we did in our Big-step normalization paper
(http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this chapter was based.

Best wishes,

James
Alan Jeffrey | 27 Oct 02:48 2011

Re: Associativity for free!

On 10/26/2011 04:01 PM, James Chapman wrote:
> 1. A trivial solution for your example is simply to make _++_ associate to the left:

Indeed. Unfortunately, sometimes it's convenient one way round, and 
sometimes the other. No matter which way you pick, it'll go wrong half 
the time :-)

> 2. Another solution I learnt from Conor (exercise 15, his AFP notes
http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it.

Hmm, I can see that this might work, though some lemmas (e.g. 
substitution commuting with weakening) would need a bit of work. Of 
course at this point having hacked out a version of lists with 
associativity, I'd like to keep pushing on it to see if I can get the 
properties I need to go through.

 > Alan: neat trick!

Thanks!

A.
James Chapman | 27 Oct 11:46 2011
Picon
Picon

Re: Associativity for free!

It strikes me that this trick works because difference lists are an embodyment of Cayley's theorem for monoids.

First some machinery:

{-# OPTIONS --type-in-type #-}

module Cayley where

data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
  refl : a ≡ a

sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
sym refl = refl

ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
ir {p = refl} {q = refl} = refl

fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}{p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'\
' → a' ≡ a''' → p ≡ q
fixtypes refl refl = ir

cong : {X Y : Set}(f : X → Y){x x' : X} → x ≡ x' → f x ≡ f x'
cong f refl = refl

id : {X : Set} → X → X
id = λ x → x

_◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
f ◦ g = λ x → f (g x)

Given any monoid (M) where the monoid laws hold propositionally:

record Monoid : Set1 where
  field set : Set
        ε   : set
        _•_ : set → set → set
        lid : ∀{m} → (ε • m) ≡ m
        rid : ∀{m} → (m • ε) ≡ m
        ass : ∀{m m' m''} → (m • (m' • m'')) ≡ ((m • m') • m'')
open Monoid

We can define a monoid (MorphMon M) where the monoid laws hold definitionally by using functions (where the
monoidal structure given by identity and composition holds definitionally).
Morph : Monoid → Set
Morph M = set M → set M

MorphMon : Monoid → Monoid
MorphMon M = record {
  set = Morph M;
  ε   = id;
  _•_ = _◦_;
  lid = refl;
  rid = refl;
  ass = refl}

Any Monoid (M, ε, _•_) is isomorphic to a subset of Morph M where the function is given by _•_ m for some m : M.

Here's a proof:

record Σ (A : Set)(P : A → Set) : Set where
  constructor _,_
  field fst : A
        snd : P fst

open Σ

eqΣ : {I : Set}{i : I}{A A' : I -> Set}{a : A i}{i' : I}{a' : A' i'} ->
          i ≡ i' -> A ≡ A' -> a ≡ a' -> _≡_ {Σ I A}(i , a) {Σ I A'}  (i' , a')
eqΣ refl refl refl = refl

record Iso (X Y : Set) : Set where
  field fun   : X → Y
        inv   : Y → X
        left  : (fun ◦ inv) ≡ id {Y}
        right : (inv ◦ fun) ≡ id {X}

postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g

Cayley : ∀ M → Iso (set M) (Σ (Morph M) λ morphM → Σ (set M) λ m → morphM ≡ _•_ M m)
Cayley M = record {
  fun   = λ m → (_•_ M m) , (m , refl);
  inv   = λ p → fst (snd p);
  left  = ext λ x → let y = sym (snd (snd x)) in eqΣ y refl (eqΣ refl (ext λ x' → cong (λ x → x ≡ (_•_ M x'))
y) (fixtypes y refl));
  right = refl}

I wonder if we can use this trick for groups as well as monoids and get difference integers, difference 'nats
(mod n)' etc. For groups we should represent them as isomorphisms (automorphims) not functions so we
would need isos to have a monodical structure which holds definitionally. But the do if we mark the field
left and right above as irrelevant:

_·_ : ∀{X Y Z} → Iso Y Z → Iso X Y → Iso X Z
f · g = record {
  fun   =  fun f ◦ fun g ;
  inv   = inv g ◦ inv f;
  left  = trans (cong (λ id → (fun f ◦ id) ◦ inv f) (left g)) (left f) ;
  right = trans (cong (λ id → (inv g ◦ id) ◦ fun g) (right f)) (right g)}

idI : ∀{X} → Iso X X
idI {X} = record {
  fun   = id;
  inv   = id;
  left  = refl;
  right = refl}

ridI : ∀{X Y}(f : Iso X Y) → (f · idI) ≡ f
ridI f = refl

lidI : ∀{X Y}(f : Iso X Y) → (idI · f) ≡ f
lidI f = refl

assI : ∀{W X Y Z}(f : Iso Y Z)(g : Iso X Y)(h : Iso W X) →
       (f · (g · h)) ≡ ((f · g) · h)
assI f g h = refl

So, it looks promising so far.

Regards,

James
James Chapman | 27 Oct 15:47 2011
Picon
Picon

Re: Associativity for free!

Next I wondered if we can generalize this from monoids to categories. For this we need Yoneda's lemma
(a.k.a. Cayley's theorem on steroids).

First an even bigger pile of suspicious looking machinery:

{-# OPTIONS --type-in-type #-}
module Yoneda where

data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
  refl : a ≡ a

sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
sym refl = refl

trans : ∀{A A' A'' : Set}{a : A}{a' : A'}{a'' : A''} →
        a ≡ a' → a' ≡ a'' → a ≡ a''
trans refl p = p

funnycong : ∀{A}{B : A → Set}{C : Set}{a a' : A} → a ≡ a' →
            .{b : B a} → .{b' : B a'} →
	    (f : (a : A) → .(B a) → C) → f a b ≡ f a' b'
funnycong refl f = refl

cong : {A B : Set}(f : A → B){a a' : A} → a ≡ a' → f a ≡ f a'
cong f refl = refl

fcong : ∀{A}{B : A → Set}{f f' : (x : A) → B x}(a : A) → f ≡ f' → f a ≡ f' a
fcong a refl = refl

ifcong : ∀{A}{B : A → Set}{f f' : {x : A} → B x}(a : A) →
         _≡_ { {x : A} → B x} f { {x : A} → B x} f' → f {a} ≡ f' {a}
ifcong a refl = refl

ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
ir {p = refl} {q = refl} = refl

fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}
           {p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'' → a' ≡ a''' → p ≡ q
fixtypes refl refl = ir

postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g

postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≡ g {a}) →
                 _≡_ { {a : A} → B a} f { {a : A} → B' a} g

id : {X : Set} → X → X
id = λ x → x

_◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
f ◦ g = λ x → f (g x)

Ok, now we define a category as follows:

record Cat : Set where
  field Obj  : Set
        Hom  : Obj → Obj → Set
        iden : ∀{X} → Hom X X
        comp : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
        idl  : ∀{X Y}{f : Hom X Y} → comp iden f ≡ f
        idr  : ∀{X Y}{f : Hom X Y} → comp f iden ≡ f
        ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
               comp (comp f g) h ≡ comp f (comp g h)
open Cat

Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:

Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)                        
Y {C} f = λ Z g → comp C g f                                                    

and we can convert back again:                                                                                

Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B                      
Y-1 {C}{A}{B} α = α B (iden C)                                                  

Given any category we can transform it like so:

CatY : Cat → Cat                                                                
CatY C = record {                                                               
  Obj  = Obj C;                                                                 
  Hom  = λ X Y → ∀ Z → Hom C Y Z → Hom C X Z;                                   
  iden = λ X → id;                                                              
  comp = λ α β Z → β Z ◦ α Z;                                                   
  idl  = refl;                                                                  
  idr  = refl;                                                                  
  ass  = refl}                                                                  

Notice we get the identities, and associativity for free.

We're sort of done unless we'd like to actually prove the isomorphism between the homsets in these
categories (Yoneda's lemma).

If we actually want to prove Yoneda's lemma we need to consider natural transformations instead of just
polymorphic functions and some more machinery:

Functors:

record Fun (C D : Cat) : Set where
  field OMap  : Obj C → Obj D
        HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
        fid   : ∀{X} → HMap (iden C {X}) ≡ iden D {OMap X}
        fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} →
                HMap (comp C f g) ≡ comp D (HMap f) (HMap g)
open Fun

The category of sets:

Sets : Cat
Sets = record{
  Obj  = Set;
  Hom  = λ X Y → X → Y;
  iden = id;
  comp = λ f g → f ◦ g;
  idl  = refl;
  idr  = refl;
  ass  = refl}

Notice the laws come from free in Sets.

Hom functors:

HomF : {C : Cat} → (A : Obj C) → Fun C Sets
HomF {C} A = record {
  OMap  = Hom C A;
  HMap  = comp C;
  fid   = ext λ _ → idl C;
  fcomp = ext λ _ → ass C}

Natural transformations:

record NatT {C D}(F G : Fun C D) : Set where
  field cmp : ∀ {X} → Hom D (OMap F X) (OMap G X)
        .nat : ∀{X Y}{f : Hom C X Y} →
              comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)

open NatT

we also define this handy principle which says that two NatTs are equal if their components are equal:

NatTEq : {C D : Cat}{F G : Fun C D}{α β : NatT F G} →
         (λ {X : Obj C} → cmp α {X}) ≡ (λ {X : Obj C} → cmp β {X}) → α ≡ β
NatTEq {C}{D}{F}{G} {α} {β} p = funnycong
  {∀ {X} → Hom D (OMap F X) (OMap G X)}
  {λ cmp → ∀{X Y}{f : Hom C X Y} →
    comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)}
  {NatT F G}
  p
  {λ{X}{Y}{f} → nat α {X}{Y}{f}}{λ{X}{Y}{f} → nat β {X}{Y}{f}}
  λ x y → record{cmp = x;nat = y}

Now we can redefine Y and Y-1 properly:

Y : ∀{C A B} → Hom C A B → NatT {C} (HomF B) (HomF A)
Y {C} f = record {
  cmp = λ g → comp C g f;
  nat = ext λ h → sym (ass C)}

Y-1 : ∀{C A B} → (NatT {C} (HomF B) (HomF A)) → Hom C A B
Y-1 {C} α = cmp α (iden C)

and prove Yoneda's lemma:

Yoneda : ∀ C A B → Iso (Hom C A B) (NatT {C} (HomF B) (HomF A))
Yoneda C A B = record {
  fun = Y {C};
  inv = Y-1 {C};
  left = ext λ α → NatTEq (iext λ Z → ext λ g → trans (fcong (iden C) (nat α))
                                                      (cong (cmp α) (idr C)));
  right = ext λ x → idl C}

Ok, I'm cheating a little, we should also prove that it is natural in A and B. Here we just proved it is an isomorphism.

I would like to get associativity and the identities for free for composition of natural transformations,
I can't have this in general as it composition uses composition in the target category of the functors
which may not come for free. But, if the target category is Sets (if we have natural transformations
between pre sheaves, which hom functors are, then it is) then we do get this stuff for free:

idNat : ∀{C}{F : Fun C Sets} → NatT F F
idNat {C}{F} = record {
  cmp = id;
  nat = refl}

compNat : ∀{C}{F G H : Fun C Sets} → NatT G H → NatT F G → NatT F H
compNat {C}{F}{G}{H} α β = record {
  cmp = cmp α ◦ cmp β;
  nat = λ{X}{Y}{f} → ext λ Z → trans (fcong (cmp β Z) (nat α {f = f}))
                                     (cong (cmp α) (fcong Z (nat β {f = f})))}

idlNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat idNat α ≡ α
idlNat {C} = refl

idrNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat α idNat ≡ α
idrNat {C}{D} = refl

assNat : ∀{C}{E F G H : Fun C Sets}{α : NatT G H}{β : NatT F G}{η : NatT E F}
         → compNat (compNat α β) η ≡ compNat α (compNat β η)
assNat {C}{D} = refl

I can fold this all up into a category CatY where the laws hold definitionally:

CatY : Cat → Cat
CatY C = record {
  Obj  = Obj C;
  Hom  = λ A B → NatT {C} (HomF B) (HomF A);
  iden = idNat;
  comp = λ α β → compNat β α;
  idl  = refl;
  idr  = refl;
  ass  = refl}

Best wishes,

James

On Oct 27, 2011, at 12:46 PM, James Chapman wrote:

> It strikes me that this trick works because difference lists are an embodyment of Cayley's theorem for monoids.
> 
> First some machinery:
> 
> {-# OPTIONS --type-in-type #-}
> 
> module Cayley where
> 
> data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
>  refl : a ≡ a
> 
> sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
> sym refl = refl
> 
> ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
> ir {p = refl} {q = refl} = refl
> 
> fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}{p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'\
> ' → a' ≡ a''' → p ≡ q
> fixtypes refl refl = ir
> 
> cong : {X Y : Set}(f : X → Y){x x' : X} → x ≡ x' → f x ≡ f x'
> cong f refl = refl
> 
> id : {X : Set} → X → X
> id = λ x → x
> 
> _◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
> f ◦ g = λ x → f (g x)
> 
> Given any monoid (M) where the monoid laws hold propositionally:
> 
> record Monoid : Set1 where
>  field set : Set
>        ε   : set
>        _•_ : set → set → set
>        lid : ∀{m} → (ε • m) ≡ m
>        rid : ∀{m} → (m • ε) ≡ m
>        ass : ∀{m m' m''} → (m • (m' • m'')) ≡ ((m • m') • m'')
> open Monoid
> 
> We can define a monoid (MorphMon M) where the monoid laws hold definitionally by using functions (where
the monoidal structure given by identity and composition holds definitionally).
> Morph : Monoid → Set
> Morph M = set M → set M
> 
> MorphMon : Monoid → Monoid
> MorphMon M = record {
>  set = Morph M;
>  ε   = id;
>  _•_ = _◦_;
>  lid = refl;
>  rid = refl;
>  ass = refl}
> 
> Any Monoid (M, ε, _•_) is isomorphic to a subset of Morph M where the function is given by _•_ m for some m
: M.
> 
> Here's a proof:
> 
> record Σ (A : Set)(P : A → Set) : Set where
>  constructor _,_
>  field fst : A
>        snd : P fst
> 
> open Σ
> 
> eqΣ : {I : Set}{i : I}{A A' : I -> Set}{a : A i}{i' : I}{a' : A' i'} ->
>          i ≡ i' -> A ≡ A' -> a ≡ a' -> _≡_ {Σ I A}(i , a) {Σ I A'}  (i' , a')
> eqΣ refl refl refl = refl
> 
> record Iso (X Y : Set) : Set where
>  field fun   : X → Y
>        inv   : Y → X
>        left  : (fun ◦ inv) ≡ id {Y}
>        right : (inv ◦ fun) ≡ id {X}
> 
> postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g
> 
> Cayley : ∀ M → Iso (set M) (Σ (Morph M) λ morphM → Σ (set M) λ m → morphM ≡ _•_ M m)
> Cayley M = record {
>  fun   = λ m → (_•_ M m) , (m , refl);
>  inv   = λ p → fst (snd p);
>  left  = ext λ x → let y = sym (snd (snd x)) in eqΣ y refl (eqΣ refl (ext λ x' → cong (λ x → x ≡ (_•_ M
x')) y) (fixtypes y refl));
>  right = refl}
> 
> I wonder if we can use this trick for groups as well as monoids and get difference integers, difference
'nats (mod n)' etc. For groups we should represent them as isomorphisms (automorphims) not functions so
we would need isos to have a monodical structure which holds definitionally. But the do if we mark the field
left and right above as irrelevant:
> 
> _·_ : ∀{X Y Z} → Iso Y Z → Iso X Y → Iso X Z
> f · g = record {
>  fun   =  fun f ◦ fun g ;
>  inv   = inv g ◦ inv f;
>  left  = trans (cong (λ id → (fun f ◦ id) ◦ inv f) (left g)) (left f) ;
>  right = trans (cong (λ id → (inv g ◦ id) ◦ fun g) (right f)) (right g)}
> 
> idI : ∀{X} → Iso X X
> idI {X} = record {
>  fun   = id;
>  inv   = id;
>  left  = refl;
>  right = refl}
> 
> ridI : ∀{X Y}(f : Iso X Y) → (f · idI) ≡ f
> ridI f = refl
> 
> lidI : ∀{X Y}(f : Iso X Y) → (idI · f) ≡ f
> lidI f = refl
> 
> assI : ∀{W X Y Z}(f : Iso Y Z)(g : Iso X Y)(h : Iso W X) →
>       (f · (g · h)) ≡ ((f · g) · h)
> assI f g h = refl
> 
> So, it looks promising so far.
> 
> Regards,
> 
> James
Andrew Cave | 27 Oct 21:06 2011
Picon

Re: Associativity for free!

Hi all,

Real cool trick!

I offer you: Cartesian categories

The object language has distinguished product objects now:

data Obj (Base : Set) : Set where
 ▹ : Base -> Obj Base
 _×_ : (X Y : Obj Base) -> Obj Base
 ⊤ : Obj Base

We just add the fields for products:

record Cat : Set where
 field Base  : Set
       Hom   : Obj Base → Obj Base → Set
       iden  : ∀{X} → Hom X X
       comp  : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
       idl   : ∀{X Y}{f : Hom X Y} → comp iden f ≡ f
       idr   : ∀{X Y}{f : Hom X Y} → comp f iden ≡ f
       ass   : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
               comp (comp f g) h ≡ comp f (comp g h)
       π₁    : ∀ {X Y} → Hom (X × Y) X
       π₂    : ∀ {X Y} → Hom (X × Y) Y
       pair  : ∀ {X Y Z} → Hom X Y → Hom X Z → Hom X (Y × Z)
       π₁β   : ∀ {X Y Z}{f : Hom X Y}{g : Hom X Z} -> comp π₁ (pair f g) ≡ f
       π₂β   : ∀ {X Y Z}{f : Hom X Y}{g : Hom X Z} -> comp π₂ (pair f g) ≡ g
       η     : ∀ {X Y Z}{f : Hom X (Y × Z)} -> f ≡ (pair (comp π₁ f)
(comp π₂ f))
       !     : ∀ {X} -> Hom X ⊤
       !η    : ∀ {X}{f g : Hom X ⊤} -> f ≡ g
open Cat

we define Homs which give us the β and η laws from Agda's products:

HomI : ∀ C (X Y : Obj (Base C)) -> Set
HomI C X (▹ B) = Hom C X (▹ B)
HomI C X (Y1 × Y2) = (HomI C X Y1) * (HomI C X Y2)
HomI C X ⊤ = Unit

Add the transformations to the Yoneda embedding; use HomI from above:

CatY : Cat → Cat
CatY C = record {
 Base  = Base C;
 Hom   = λ X Y → ∀ Z → HomI C Z X → HomI C Z Y;
 iden  = λ Z -> id;
 comp  = λ α β Z → (α Z) ◦ (β Z);
 idl   = refl;
 idr   = refl;
 ass   = refl;
 π₁    = λ Z -> _*_.fst;
 π₂    = λ Z -> _*_.snd;
 pair  = λ f g Z x → (f Z x , g Z x);
 π₁β   = refl;
 π₂β   = refl;
 η     = refl;
 !     = λ Z x → tt;
 !η    = refl
 }

And we get the beta and eta laws for free!

After much fighting with implicit arguments, realizing I don't know
how to use modules properly, setting up some definitions instead, etc,
it managed to prove a nasty example:

test : ∀ {Γ Δ S T} {σ : HomY Δ Γ} {N : HomY Γ T} {M : HomY (Γ × T) S}
        -> (M ∘ ([ id , N ] ∘ σ)) ≡ ((M ∘ [ σ ∘ π1 , π2 ]) ∘ [ id , (N ∘ σ) ])
test = refl

This example comes from the proof of the substitution lemma for object
languages with dependent types. Next goal is to see if I can harness
this...

Regards,
Andrew

On Thu, Oct 27, 2011 at 9:47 AM, James Chapman <james@...> wrote:
> Next I wondered if we can generalize this from monoids to categories. For this we need Yoneda's lemma
(a.k.a. Cayley's theorem on steroids).
>
> First an even bigger pile of suspicious looking machinery:
>
> {-# OPTIONS --type-in-type #-}
> module Yoneda where
>
> data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
>  refl : a ≡ a
>
> sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
> sym refl = refl
>
> trans : ∀{A A' A'' : Set}{a : A}{a' : A'}{a'' : A''} →
>        a ≡ a' → a' ≡ a'' → a ≡ a''
> trans refl p = p
>
> funnycong : ∀{A}{B : A → Set}{C : Set}{a a' : A} → a ≡ a' →
>            .{b : B a} → .{b' : B a'} →
>            (f : (a : A) → .(B a) → C) → f a b ≡ f a' b'
> funnycong refl f = refl
>
> cong : {A B : Set}(f : A → B){a a' : A} → a ≡ a' → f a ≡ f a'
> cong f refl = refl
>
> fcong : ∀{A}{B : A → Set}{f f' : (x : A) → B x}(a : A) → f ≡ f' → f a ≡ f' a
> fcong a refl = refl
>
> ifcong : ∀{A}{B : A → Set}{f f' : {x : A} → B x}(a : A) →
>         _≡_ { {x : A} → B x} f { {x : A} → B x} f' → f {a} ≡ f' {a}
> ifcong a refl = refl
>
> ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
> ir {p = refl} {q = refl} = refl
>
> fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}
>           {p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'' → a' ≡ a''' → p ≡ q
> fixtypes refl refl = ir
>
> postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g
>
> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
>                 (∀ a → f {a} ≡ g {a}) →
>                 _≡_ { {a : A} → B a} f { {a : A} → B' a} g
>
> id : {X : Set} → X → X
> id = λ x → x
>
> _◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
> f ◦ g = λ x → f (g x)
>
> Ok, now we define a category as follows:
>
> record Cat : Set where
>  field Obj  : Set
>        Hom  : Obj → Obj → Set
>        iden : ∀{X} → Hom X X
>        comp : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
>        idl  : ∀{X Y}{f : Hom X Y} → comp iden f ≡ f
>        idr  : ∀{X Y}{f : Hom X Y} → comp f iden ≡ f
>        ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
>               comp (comp f g) h ≡ comp f (comp g h)
> open Cat
>
> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>
> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> Y {C} f = λ Z g → comp C g f
>
> and we can convert back again:
>
> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> Y-1 {C}{A}{B} α = α B (iden C)
>
> Given any category we can transform it like so:
>
> CatY : Cat → Cat
> CatY C = record {
>  Obj  = Obj C;
>  Hom  = λ X Y → ∀ Z → Hom C Y Z → Hom C X Z;
>  iden = λ X → id;
>  comp = λ α β Z → β Z ◦ α Z;
>  idl  = refl;
>  idr  = refl;
>  ass  = refl}
>
> Notice we get the identities, and associativity for free.
>
> We're sort of done unless we'd like to actually prove the isomorphism between the homsets in these
categories (Yoneda's lemma).
>
> If we actually want to prove Yoneda's lemma we need to consider natural transformations instead of just
polymorphic functions and some more machinery:
>
> Functors:
>
> record Fun (C D : Cat) : Set where
>  field OMap  : Obj C → Obj D
>        HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
>        fid   : ∀{X} → HMap (iden C {X}) ≡ iden D {OMap X}
>        fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} →
>                HMap (comp C f g) ≡ comp D (HMap f) (HMap g)
> open Fun
>
> The category of sets:
>
> Sets : Cat
> Sets = record{
>  Obj  = Set;
>  Hom  = λ X Y → X → Y;
>  iden = id;
>  comp = λ f g → f ◦ g;
>  idl  = refl;
>  idr  = refl;
>  ass  = refl}
>
> Notice the laws come from free in Sets.
>
> Hom functors:
>
> HomF : {C : Cat} → (A : Obj C) → Fun C Sets
> HomF {C} A = record {
>  OMap  = Hom C A;
>  HMap  = comp C;
>  fid   = ext λ _ → idl C;
>  fcomp = ext λ _ → ass C}
>
> Natural transformations:
>
> record NatT {C D}(F G : Fun C D) : Set where
>  field cmp : ∀ {X} → Hom D (OMap F X) (OMap G X)
>        .nat : ∀{X Y}{f : Hom C X Y} →
>              comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)
>
> open NatT
>
> we also define this handy principle which says that two NatTs are equal if their components are equal:
>
> NatTEq : {C D : Cat}{F G : Fun C D}{α β : NatT F G} →
>         (λ {X : Obj C} → cmp α {X}) ≡ (λ {X : Obj C} → cmp β {X}) → α ≡ β
> NatTEq {C}{D}{F}{G} {α} {β} p = funnycong
>  {∀ {X} → Hom D (OMap F X) (OMap G X)}
>  {λ cmp → ∀{X Y}{f : Hom C X Y} →
>    comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)}
>  {NatT F G}
>  p
>  {λ{X}{Y}{f} → nat α {X}{Y}{f}}{λ{X}{Y}{f} → nat β {X}{Y}{f}}
>  λ x y → record{cmp = x;nat = y}
>
> Now we can redefine Y and Y-1 properly:
>
> Y : ∀{C A B} → Hom C A B → NatT {C} (HomF B) (HomF A)
> Y {C} f = record {
>  cmp = λ g → comp C g f;
>  nat = ext λ h → sym (ass C)}
>
> Y-1 : ∀{C A B} → (NatT {C} (HomF B) (HomF A)) → Hom C A B
> Y-1 {C} α = cmp α (iden C)
>
> and prove Yoneda's lemma:
>
> Yoneda : ∀ C A B → Iso (Hom C A B) (NatT {C} (HomF B) (HomF A))
> Yoneda C A B = record {
>  fun = Y {C};
>  inv = Y-1 {C};
>  left = ext λ α → NatTEq (iext λ Z → ext λ g → trans (fcong (iden C) (nat α))
>                                                      (cong (cmp α) (idr C)));
>  right = ext λ x → idl C}
>
> Ok, I'm cheating a little, we should also prove that it is natural in A and B. Here we just proved it is an isomorphism.
>
> I would like to get associativity and the identities for free for composition of natural
transformations, I can't have this in general as it composition uses composition in the target category
of the functors which may not come for free. But, if the target category is Sets (if we have natural
transformations between pre sheaves, which hom functors are, then it is) then we do get this stuff for free:
>
> idNat : ∀{C}{F : Fun C Sets} → NatT F F
> idNat {C}{F} = record {
>  cmp = id;
>  nat = refl}
>
> compNat : ∀{C}{F G H : Fun C Sets} → NatT G H → NatT F G → NatT F H
> compNat {C}{F}{G}{H} α β = record {
>  cmp = cmp α ◦ cmp β;
>  nat = λ{X}{Y}{f} → ext λ Z → trans (fcong (cmp β Z) (nat α {f = f}))
>                                     (cong (cmp α) (fcong Z (nat β {f = f})))}
>
> idlNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat idNat α ≡ α
> idlNat {C} = refl
>
> idrNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat α idNat ≡ α
> idrNat {C}{D} = refl
>
> assNat : ∀{C}{E F G H : Fun C Sets}{α : NatT G H}{β : NatT F G}{η : NatT E F}
>         → compNat (compNat α β) η ≡ compNat α (compNat β η)
> assNat {C}{D} = refl
>
> I can fold this all up into a category CatY where the laws hold definitionally:
>
> CatY : Cat → Cat
> CatY C = record {
>  Obj  = Obj C;
>  Hom  = λ A B → NatT {C} (HomF B) (HomF A);
>  iden = idNat;
>  comp = λ α β → compNat β α;
>  idl  = refl;
>  idr  = refl;
>  ass  = refl}
>
> Best wishes,
>
> James
>
> On Oct 27, 2011, at 12:46 PM, James Chapman wrote:
>
>> It strikes me that this trick works because difference lists are an embodyment of Cayley's theorem for monoids.
>>
>> First some machinery:
>>
>> {-# OPTIONS --type-in-type #-}
>>
>> module Cayley where
>>
>> data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
>>  refl : a ≡ a
>>
>> sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
>> sym refl = refl
>>
>> ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
>> ir {p = refl} {q = refl} = refl
>>
>> fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}{p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'\
>> ' → a' ≡ a''' → p ≡ q
>> fixtypes refl refl = ir
>>
>> cong : {X Y : Set}(f : X → Y){x x' : X} → x ≡ x' → f x ≡ f x'
>> cong f refl = refl
>>
>> id : {X : Set} → X → X
>> id = λ x → x
>>
>> _◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
>> f ◦ g = λ x → f (g x)
>>
>> Given any monoid (M) where the monoid laws hold propositionally:
>>
>> record Monoid : Set1 where
>>  field set : Set
>>        ε   : set
>>        _•_ : set → set → set
>>        lid : ∀{m} → (ε • m) ≡ m
>>        rid : ∀{m} → (m • ε) ≡ m
>>        ass : ∀{m m' m''} → (m • (m' • m'')) ≡ ((m • m') • m'')
>> open Monoid
>>
>> We can define a monoid (MorphMon M) where the monoid laws hold definitionally by using functions (where
the monoidal structure given by identity and composition holds definitionally).
>> Morph : Monoid → Set
>> Morph M = set M → set M
>>
>> MorphMon : Monoid → Monoid
>> MorphMon M = record {
>>  set = Morph M;
>>  ε   = id;
>>  _•_ = _◦_;
>>  lid = refl;
>>  rid = refl;
>>  ass = refl}
>>
>> Any Monoid (M, ε, _•_) is isomorphic to a subset of Morph M where the function is given by _•_ m for some
m : M.
>>
>> Here's a proof:
>>
>> record Σ (A : Set)(P : A → Set) : Set where
>>  constructor _,_
>>  field fst : A
>>        snd : P fst
>>
>> open Σ
>>
>> eqΣ : {I : Set}{i : I}{A A' : I -> Set}{a : A i}{i' : I}{a' : A' i'} ->
>>          i ≡ i' -> A ≡ A' -> a ≡ a' -> _≡_ {Σ I A}(i , a) {Σ I A'}  (i' , a')
>> eqΣ refl refl refl = refl
>>
>> record Iso (X Y : Set) : Set where
>>  field fun   : X → Y
>>        inv   : Y → X
>>        left  : (fun ◦ inv) ≡ id {Y}
>>        right : (inv ◦ fun) ≡ id {X}
>>
>> postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g
>>
>> Cayley : ∀ M → Iso (set M) (Σ (Morph M) λ morphM → Σ (set M) λ m → morphM ≡ _•_ M m)
>> Cayley M = record {
>>  fun   = λ m → (_•_ M m) , (m , refl);
>>  inv   = λ p → fst (snd p);
>>  left  = ext λ x → let y = sym (snd (snd x)) in eqΣ y refl (eqΣ refl (ext λ x' → cong (λ x → x ≡
(_•_ M x')) y) (fixtypes y refl));
>>  right = refl}
>>
>> I wonder if we can use this trick for groups as well as monoids and get difference integers, difference
'nats (mod n)' etc. For groups we should represent them as isomorphisms (automorphims) not functions so
we would need isos to have a monodical structure which holds definitionally. But the do if we mark the field
left and right above as irrelevant:
>>
>> _·_ : ∀{X Y Z} → Iso Y Z → Iso X Y → Iso X Z
>> f · g = record {
>>  fun   =  fun f ◦ fun g ;
>>  inv   = inv g ◦ inv f;
>>  left  = trans (cong (λ id → (fun f ◦ id) ◦ inv f) (left g)) (left f) ;
>>  right = trans (cong (λ id → (inv g ◦ id) ◦ fun g) (right f)) (right g)}
>>
>> idI : ∀{X} → Iso X X
>> idI {X} = record {
>>  fun   = id;
>>  inv   = id;
>>  left  = refl;
>>  right = refl}
>>
>> ridI : ∀{X Y}(f : Iso X Y) → (f · idI) ≡ f
>> ridI f = refl
>>
>> lidI : ∀{X Y}(f : Iso X Y) → (idI · f) ≡ f
>> lidI f = refl
>>
>> assI : ∀{W X Y Z}(f : Iso Y Z)(g : Iso X Y)(h : Iso W X) →
>>       (f · (g · h)) ≡ ((f · g) · h)
>> assI f g h = refl
>>
>> So, it looks promising so far.
>>
>> Regards,
>>
>> James
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
Alan Jeffrey | 27 Oct 23:41 2011

Re: Associativity for free!

OK, that's pretty cool.

One thing which did occur to me (though I didn't persue it very far) is 
that there's a connection with n-categorical machinery.

Recall that the equivalence (ok : f ≡ _++_ as) had to be declared 
irrelevant, because otherwise its proof objects were causing 
associativity to fail. Well, we could (of course, who would do anything 
else :-) do the same trick one level up, and replace ok by a function 
something like (ok1 : ∀ bs g → (g ≡ _++_ bs) → ((g ◦ f) ≡ _++_ (g as))), 
that is ok1 proves that composition with f transforms 
appending-functions to appending-functions. In particular, ok is (ok1 [] 
id refl).

Oh, but now we're not isomorphic to lists any more, because there's too 
many ok1 functions, so we need an ok2 which says that ok1 is "the 
obvious proof given ok". Ah, but then ok2 needs to be irrelevant. Or we 
play the same trick again and define ok3 (etc. etc. etc.)

This all has the flavor of an n-category where you have n levels of 
canonical isomorphisms, with a base case of definitional equality.

It would take a braver person than I to try to persuade Agda of this though.

A.

On 10/27/2011 08:47 AM, James Chapman wrote:
> Next I wondered if we can generalize this from monoids to categories. For this we need Yoneda's lemma
(a.k.a. Cayley's theorem on steroids).
>
> First an even bigger pile of suspicious looking machinery:
>
> {-# OPTIONS --type-in-type #-}
> module Yoneda where
>
> data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
>    refl : a ≡ a
>
> sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
> sym refl = refl
>
> trans : ∀{A A' A'' : Set}{a : A}{a' : A'}{a'' : A''} →
>          a ≡ a' → a' ≡ a'' → a ≡ a''
> trans refl p = p
>
> funnycong : ∀{A}{B : A → Set}{C : Set}{a a' : A} → a ≡ a' →
>              .{b : B a} → .{b' : B a'} →
> 	    (f : (a : A) → .(B a) → C) → f a b ≡ f a' b'
> funnycong refl f = refl
>
> cong : {A B : Set}(f : A → B){a a' : A} → a ≡ a' → f a ≡ f a'
> cong f refl = refl
>
> fcong : ∀{A}{B : A → Set}{f f' : (x : A) → B x}(a : A) → f ≡ f' → f a ≡ f' a
> fcong a refl = refl
>
> ifcong : ∀{A}{B : A → Set}{f f' : {x : A} → B x}(a : A) →
>           _≡_ { {x : A} → B x} f { {x : A} → B x} f' → f {a} ≡ f' {a}
> ifcong a refl = refl
>
> ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
> ir {p = refl} {q = refl} = refl
>
> fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}
>             {p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'' → a' ≡ a''' → p ≡ q
> fixtypes refl refl = ir
>
> postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g
>
> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
>                   (∀ a → f {a} ≡ g {a}) →
>                   _≡_ { {a : A} → B a} f { {a : A} → B' a} g
>
> id : {X : Set} → X → X
> id = λ x → x
>
> _◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
> f ◦ g = λ x → f (g x)
>
> Ok, now we define a category as follows:
>
> record Cat : Set where
>    field Obj  : Set
>          Hom  : Obj → Obj → Set
>          iden : ∀{X} → Hom X X
>          comp : ∀{X Y Z} → Hom Y Z → Hom X Y → Hom X Z
>          idl  : ∀{X Y}{f : Hom X Y} → comp iden f ≡ f
>          idr  : ∀{X Y}{f : Hom X Y} → comp f iden ≡ f
>          ass  : ∀{W X Y Z}{f : Hom Y Z}{g : Hom X Y}{h : Hom W X} →
>                 comp (comp f g) h ≡ comp f (comp g h)
> open Cat
>
> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>
> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> Y {C} f = λ Z g → comp C g f
>
> and we can convert back again:
>
> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> Y-1 {C}{A}{B} α = α B (iden C)
>
> Given any category we can transform it like so:
>
> CatY : Cat → Cat
> CatY C = record {
>    Obj  = Obj C;
>    Hom  = λ X Y → ∀ Z → Hom C Y Z → Hom C X Z;
>    iden = λ X → id;
>    comp = λ α β Z → β Z ◦ α Z;
>    idl  = refl;
>    idr  = refl;
>    ass  = refl}
>
> Notice we get the identities, and associativity for free.
>
> We're sort of done unless we'd like to actually prove the isomorphism between the homsets in these
categories (Yoneda's lemma).
>
> If we actually want to prove Yoneda's lemma we need to consider natural transformations instead of just
polymorphic functions and some more machinery:
>
> Functors:
>
> record Fun (C D : Cat) : Set where
>    field OMap  : Obj C → Obj D
>          HMap  : ∀{X Y} → Hom C X Y → Hom D (OMap X) (OMap Y)
>          fid   : ∀{X} → HMap (iden C {X}) ≡ iden D {OMap X}
>          fcomp : ∀{X Y Z}{f : Hom C Y Z}{g : Hom C X Y} →
>                  HMap (comp C f g) ≡ comp D (HMap f) (HMap g)
> open Fun
>
> The category of sets:
>
> Sets : Cat
> Sets = record{
>    Obj  = Set;
>    Hom  = λ X Y → X → Y;
>    iden = id;
>    comp = λ f g → f ◦ g;
>    idl  = refl;
>    idr  = refl;
>    ass  = refl}
>
> Notice the laws come from free in Sets.
>
> Hom functors:
>
> HomF : {C : Cat} → (A : Obj C) → Fun C Sets
> HomF {C} A = record {
>    OMap  = Hom C A;
>    HMap  = comp C;
>    fid   = ext λ _ → idl C;
>    fcomp = ext λ _ → ass C}
>
> Natural transformations:
>
> record NatT {C D}(F G : Fun C D) : Set where
>    field cmp : ∀ {X} → Hom D (OMap F X) (OMap G X)
>          .nat : ∀{X Y}{f : Hom C X Y} →
>                comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)
>
> open NatT
>
> we also define this handy principle which says that two NatTs are equal if their components are equal:
>
> NatTEq : {C D : Cat}{F G : Fun C D}{α β : NatT F G} →
>           (λ {X : Obj C} → cmp α {X}) ≡ (λ {X : Obj C} → cmp β {X}) → α ≡ β
> NatTEq {C}{D}{F}{G} {α} {β} p = funnycong
>    {∀ {X} → Hom D (OMap F X) (OMap G X)}
>    {λ cmp → ∀{X Y}{f : Hom C X Y} →
>      comp D (HMap G f) cmp ≡ comp D cmp (HMap F f)}
>    {NatT F G}
>    p
>    {λ{X}{Y}{f} → nat α {X}{Y}{f}}{λ{X}{Y}{f} → nat β {X}{Y}{f}}
>    λ x y → record{cmp = x;nat = y}
>
> Now we can redefine Y and Y-1 properly:
>
> Y : ∀{C A B} → Hom C A B → NatT {C} (HomF B) (HomF A)
> Y {C} f = record {
>    cmp = λ g → comp C g f;
>    nat = ext λ h → sym (ass C)}
>
> Y-1 : ∀{C A B} → (NatT {C} (HomF B) (HomF A)) → Hom C A B
> Y-1 {C} α = cmp α (iden C)
>
> and prove Yoneda's lemma:
>
> Yoneda : ∀ C A B → Iso (Hom C A B) (NatT {C} (HomF B) (HomF A))
> Yoneda C A B = record {
>    fun = Y {C};
>    inv = Y-1 {C};
>    left = ext λ α → NatTEq (iext λ Z → ext λ g → trans (fcong (iden C) (nat α))
>                                                        (cong (cmp α) (idr C)));
>    right = ext λ x → idl C}
>
> Ok, I'm cheating a little, we should also prove that it is natural in A and B. Here we just proved it is an isomorphism.
>
> I would like to get associativity and the identities for free for composition of natural
transformations, I can't have this in general as it composition uses composition in the target category
of the functors which may not come for free. But, if the target category is Sets (if we have natural
transformations between pre sheaves, which hom functors are, then it is) then we do get this stuff for free:
>
> idNat : ∀{C}{F : Fun C Sets} → NatT F F
> idNat {C}{F} = record {
>    cmp = id;
>    nat = refl}
>
> compNat : ∀{C}{F G H : Fun C Sets} → NatT G H → NatT F G → NatT F H
> compNat {C}{F}{G}{H} α β = record {
>    cmp = cmp α ◦ cmp β;
>    nat = λ{X}{Y}{f} → ext λ Z → trans (fcong (cmp β Z) (nat α {f = f}))
>                                       (cong (cmp α) (fcong Z (nat β {f = f})))}
>
> idlNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat idNat α ≡ α
> idlNat {C} = refl
>
> idrNat : ∀{C}{F G : Fun C Sets}{α : NatT F G} → compNat α idNat ≡ α
> idrNat {C}{D} = refl
>
> assNat : ∀{C}{E F G H : Fun C Sets}{α : NatT G H}{β : NatT F G}{η : NatT E F}
>           → compNat (compNat α β) η ≡ compNat α (compNat β η)
> assNat {C}{D} = refl
>
> I can fold this all up into a category CatY where the laws hold definitionally:
>
> CatY : Cat → Cat
> CatY C = record {
>    Obj  = Obj C;
>    Hom  = λ A B → NatT {C} (HomF B) (HomF A);
>    iden = idNat;
>    comp = λ α β → compNat β α;
>    idl  = refl;
>    idr  = refl;
>    ass  = refl}
>
> Best wishes,
>
> James
>
> On Oct 27, 2011, at 12:46 PM, James Chapman wrote:
>
>> It strikes me that this trick works because difference lists are an embodyment of Cayley's theorem for monoids.
>>
>> First some machinery:
>>
>> {-# OPTIONS --type-in-type #-}
>>
>> module Cayley where
>>
>> data _≡_ {A : Set}(a : A) : {A' : Set} → A' → Set where
>>   refl : a ≡ a
>>
>> sym : ∀{A A' : Set}{a : A}{a' : A'} → a ≡ a' → a' ≡ a
>> sym refl = refl
>>
>> ir : ∀{A A'}{a : A}{a' : A'}{p q : a ≡ a'} → p ≡ q
>> ir {p = refl} {q = refl} = refl
>>
>> fixtypes : ∀{A A' : Set}{a a' : A}{a'' a''' : A'}{p : a ≡ a'}{q : a'' ≡ a'''} → a ≡ a'\
>> ' → a' ≡ a''' → p ≡ q
>> fixtypes refl refl = ir
>>
>> cong : {X Y : Set}(f : X → Y){x x' : X} → x ≡ x' → f x ≡ f x'
>> cong f refl = refl
>>
>> id : {X : Set} → X → X
>> id = λ x → x
>>
>> _◦_ : {X Y Z : Set} → (Y → Z) → (X → Y) → X → Z
>> f ◦ g = λ x → f (g x)
>>
>> Given any monoid (M) where the monoid laws hold propositionally:
>>
>> record Monoid : Set1 where
>>   field set : Set
>>         ε   : set
>>         _•_ : set → set → set
>>         lid : ∀{m} → (ε • m) ≡ m
>>         rid : ∀{m} → (m • ε) ≡ m
>>         ass : ∀{m m' m''} → (m • (m' • m'')) ≡ ((m • m') • m'')
>> open Monoid
>>
>> We can define a monoid (MorphMon M) where the monoid laws hold definitionally by using functions (where
the monoidal structure given by identity and composition holds definitionally).
>> Morph : Monoid → Set
>> Morph M = set M → set M
>>
>> MorphMon : Monoid → Monoid
>> MorphMon M = record {
>>   set = Morph M;
>>   ε   = id;
>>   _•_ = _◦_;
>>   lid = refl;
>>   rid = refl;
>>   ass = refl}
>>
>> Any Monoid (M, ε, _•_) is isomorphic to a subset of Morph M where the function is given by _•_ m for some
m : M.
>>
>> Here's a proof:
>>
>> record Σ (A : Set)(P : A → Set) : Set where
>>   constructor _,_
>>   field fst : A
>>         snd : P fst
>>
>> open Σ
>>
>> eqΣ : {I : Set}{i : I}{A A' : I ->  Set}{a : A i}{i' : I}{a' : A' i'} ->
>>           i ≡ i' ->  A ≡ A' ->  a ≡ a' ->  _≡_ {Σ I A}(i , a) {Σ I A'}  (i' , a')
>> eqΣ refl refl refl = refl
>>
>> record Iso (X Y : Set) : Set where
>>   field fun   : X → Y
>>         inv   : Y → X
>>         left  : (fun ◦ inv) ≡ id {Y}
>>         right : (inv ◦ fun) ≡ id {X}
>>
>> postulate ext : {X Y : Set}{f g : X → Y} → (∀ x → f x ≡ g x) → f ≡ g
>>
>> Cayley : ∀ M → Iso (set M) (Σ (Morph M) λ morphM → Σ (set M) λ m → morphM ≡ _•_ M m)
>> Cayley M = record {
>>   fun   = λ m → (_•_ M m) , (m , refl);
>>   inv   = λ p → fst (snd p);
>>   left  = ext λ x → let y = sym (snd (snd x)) in eqΣ y refl (eqΣ refl (ext λ x' → cong (λ x → x ≡ (_•_ M
x')) y) (fixtypes y refl));
>>   right = refl}
>>
>> I wonder if we can use this trick for groups as well as monoids and get difference integers, difference
'nats (mod n)' etc. For groups we should represent them as isomorphisms (automorphims) not functions so
we would need isos to have a monodical structure which holds definitionally. But the do if we mark the field
left and right above as irrelevant:
>>
>> _·_ : ∀{X Y Z} → Iso Y Z → Iso X Y → Iso X Z
>> f · g = record {
>>   fun   =  fun f ◦ fun g ;
>>   inv   = inv g ◦ inv f;
>>   left  = trans (cong (λ id → (fun f ◦ id) ◦ inv f) (left g)) (left f) ;
>>   right = trans (cong (λ id → (inv g ◦ id) ◦ fun g) (right f)) (right g)}
>>
>> idI : ∀{X} → Iso X X
>> idI {X} = record {
>>   fun   = id;
>>   inv   = id;
>>   left  = refl;
>>   right = refl}
>>
>> ridI : ∀{X Y}(f : Iso X Y) → (f · idI) ≡ f
>> ridI f = refl
>>
>> lidI : ∀{X Y}(f : Iso X Y) → (idI · f) ≡ f
>> lidI f = refl
>>
>> assI : ∀{W X Y Z}(f : Iso Y Z)(g : Iso X Y)(h : Iso W X) →
>>        (f · (g · h)) ≡ ((f · g) · h)
>> assI f g h = refl
>>
>> So, it looks promising so far.
>>
>> Regards,
>>
>> James
>
Andreas Abel | 28 Oct 17:26 2011
Picon

Re: Associativity for free!

On 10/27/11 3:47 PM, James Chapman wrote:
> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>
> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> Y {C} f = λ Z g → comp C g f
>
> and we can convert back again:
>
> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> Y-1 {C}{A}{B} α = α B (iden C)

Is that the glorious Yoneda lemma?  Trivial in the language of types. 
Just subtract the categorical waffle and every programmer understands it...

Cheers,
Andreas

--

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

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

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
Alan Jeffrey | 28 Oct 19:55 2011

Re: Associativity for free!

That's the Glorious Yoneda Lemma's action on homs, you are also expected 
to prove a bunch of coherence properties. I suspect that if we assumed 
parametricity of Agda, then many of the coherence properties would come 
out in the wash.

I prefer categorical waffles to burned toast, which is often the 
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> On 10/27/11 3:47 PM, James Chapman wrote:
>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>
>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>> Y {C} f = λ Z g → comp C g f
>>
>> and we can convert back again:
>>
>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>> Y-1 {C}{A}{B} α = α B (iden C)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types.
> Just subtract the categorical waffle and every programmer understands it...
>
> Cheers,
> Andreas
>
Peter Dybjer | 28 Oct 20:23 2011
Picon
Picon

RE: Associativity for free!

Have a look at

http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf

I think it is related.
Peter

________________________________________
From: agda-bounces@...
[agda-bounces@...] On Behalf Of Alan Jeffrey [ajeffrey@...]
Sent: Friday, October 28, 2011 7:55 PM
To: Andreas Abel
Cc: Agda mailing list
Subject: Re: [Agda] Associativity for free!

That's the Glorious Yoneda Lemma's action on homs, you are also expected
to prove a bunch of coherence properties. I suspect that if we assumed
parametricity of Agda, then many of the coherence properties would come
out in the wash.

I prefer categorical waffles to burned toast, which is often the
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> On 10/27/11 3:47 PM, James Chapman wrote:
>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>
>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>> Y {C} f = λ Z g → comp C g f
>>
>> and we can convert back again:
>>
>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>> Y-1 {C}{A}{B} α = α B (iden C)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types.
> Just subtract the categorical waffle and every programmer understands it...
>
> Cheers,
> Andreas
>
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Daniel Peebles | 28 Oct 20:39 2011
Picon

Re: Associativity for free!

That link looks broken, but http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf seemed to work :)


2011/10/28 Peter Dybjer <peterd-Ga8gg/MwtDQwFerOooGFRg@public.gmane.org>
Have a look at

http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf

I think it is related.
Peter

________________________________________
From: agda-bounces <at> lists.chalmers.se [agda-bounces-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org] On Behalf Of Alan Jeffrey [ajeffrey-zWi12Q5vYqaakBO8gow8eQ@public.gmane.org]
Sent: Friday, October 28, 2011 7:55 PM
To: Andreas Abel
Cc: Agda mailing list
Subject: Re: [Agda] Associativity for free!

That's the Glorious Yoneda Lemma's action on homs, you are also expected
to prove a bunch of coherence properties. I suspect that if we assumed
parametricity of Agda, then many of the coherence properties would come
out in the wash.

I prefer categorical waffles to burned toast, which is often the
alternative.

A.

On 10/28/2011 10:26 AM, Andreas Abel wrote:
> On 10/27/11 3:47 PM, James Chapman wrote:
>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>
>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>> Y {C} f = λ Z g → comp C g f
>>
>> and we can convert back again:
>>
>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>> Y-1 {C}{A}{B} α = α B (iden C)
>
> Is that the glorious Yoneda lemma?  Trivial in the language of types.
> Just subtract the categorical waffle and every programmer understands it...
>
> Cheers,
> Andreas
>
_______________________________________________
Agda mailing list
Agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda
_______________________________________________
Agda mailing list
Agda-TrQ0NnR75azkdzWRgU60H7NAH6kLmebB@public.gmane.org
https://lists.chalmers.se/mailman/listinfo/agda

_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Alan Jeffrey | 28 Oct 20:49 2011

Re: Associativity for free!

Oops, URL typo...

   http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf

I had a quick read through, and it is indeed related, but (I believe) 
is, given any monoid (resp. monoidal category) M, building a strict 
monoid (resp. strict monoidal category) N and a morphism (resp. monoidal 
functor) J : M -> N such that (a ~ b in M) iff (J a = J b).

This is indeed related. The thing I think might be new is using 
irrelevance as a way to build the subset of N such that J forms an 
isomorphism.

A.

On 10/28/2011 01:23 PM, Peter Dybjer wrote:
> Have a look at
>
> http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf
>
> I think it is related.
> Peter
>
> ________________________________________
> From: agda-bounces@...
[agda-bounces@...] On Behalf Of Alan Jeffrey [ajeffrey@...]
> Sent: Friday, October 28, 2011 7:55 PM
> To: Andreas Abel
> Cc: Agda mailing list
> Subject: Re: [Agda] Associativity for free!
>
> That's the Glorious Yoneda Lemma's action on homs, you are also expected
> to prove a bunch of coherence properties. I suspect that if we assumed
> parametricity of Agda, then many of the coherence properties would come
> out in the wash.
>
> I prefer categorical waffles to burned toast, which is often the
> alternative.
>
> A.
>
> On 10/28/2011 10:26 AM, Andreas Abel wrote:
>> On 10/27/11 3:47 PM, James Chapman wrote:
>>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>>
>>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>>> Y {C} f = λ Z g → comp C g f
>>>
>>> and we can convert back again:
>>>
>>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>>> Y-1 {C}{A}{B} α = α B (iden C)
>>
>> Is that the glorious Yoneda lemma?  Trivial in the language of types.
>> Just subtract the categorical waffle and every programmer understands it...
>>
>> Cheers,
>> Andreas
>>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
Alan Jeffrey | 28 Oct 21:40 2011

Re: Associativity for free!

Hmm, thinking of which, this means that adding:

   ≡-relevant : ∀ {A} {a b : A} → .(a ≡ b) → (a ≡ b)

means that given f : A → B, we can define a subset of B isomorphic to 
the image of f as:

   record Image {A B : Set} (f : A → B) : Set where
     b : B
     .b✓ : ∃ (λ a → f a ≡ b)

The "assoiativity for free" construction for a monoid (_+_ : A → A → A) 
is just (Image _+_).

A.

On 10/28/2011 01:49 PM, Jeffrey, Alan S A (Alan) wrote:
> Oops, URL typo...
>
>     http://www.cse.chalmers.se/~peterd/papers/Coherence_Monoidal.pdf
>
> I had a quick read through, and it is indeed related, but (I believe)
> is, given any monoid (resp. monoidal category) M, building a strict
> monoid (resp. strict monoidal category) N and a morphism (resp. monoidal
> functor) J : M ->  N such that (a ~ b in M) iff (J a = J b).
>
> This is indeed related. The thing I think might be new is using
> irrelevance as a way to build the subset of N such that J forms an
> isomorphism.
>
> A.
>
> On 10/28/2011 01:23 PM, Peter Dybjer wrote:
>> Have a look at
>>
>> http://www.cse.chalmers.se/~peterd/papers/nbe.html/Coherence_Monoidal.pdf
>>
>> I think it is related.
>> Peter
>>
>> ________________________________________
>> From: agda-bounces@...
[agda-bounces@...] On Behalf Of Alan Jeffrey [ajeffrey@...]
>> Sent: Friday, October 28, 2011 7:55 PM
>> To: Andreas Abel
>> Cc: Agda mailing list
>> Subject: Re: [Agda] Associativity for free!
>>
>> That's the Glorious Yoneda Lemma's action on homs, you are also expected
>> to prove a bunch of coherence properties. I suspect that if we assumed
>> parametricity of Agda, then many of the coherence properties would come
>> out in the wash.
>>
>> I prefer categorical waffles to burned toast, which is often the
>> alternative.
>>
>> A.
>>
>> On 10/28/2011 10:26 AM, Andreas Abel wrote:
>>> On 10/27/11 3:47 PM, James Chapman wrote:
>>>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>>>
>>>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>>>> Y {C} f = λ Z g → comp C g f
>>>>
>>>> and we can convert back again:
>>>>
>>>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>>>> Y-1 {C}{A}{B} α = α B (iden C)
>>>
>>> Is that the glorious Yoneda lemma?  Trivial in the language of types.
>>> Just subtract the categorical waffle and every programmer understands it...
>>>
>>> Cheers,
>>> Andreas
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
KINOSHITA Yoshiki | 1 Nov 13:57 2011
Picon

Re: [yoshiki] Re: Associativity for free!

Dear Andreas,

surely, what James described is a part of (gateway to?) Yoneda lemma.

I think you are right in saying that it is trivial.  The whole body of
Yoneda lemma is trivial.  I recall Peter Freyd wrote something which
means that many theorems in category theory are trivial, but it is not
trivial to find a setting which makes those things trivial.  I am sure
Freyd's original wording was much better.  I once read it in some
mailing list, was impressed by it, talked about it with several
people, lost the article and have never found it again.  I miss it...

Yoshiki.
--
Yoshiki Kinoshita, D.Sc.
Principal Research Scientist
Information Technology Research Insititute
National Institute of Advanced Industrial Science and Technology (AIST)
3-11-46 Nakoji, Amagasaki-shi
Hyogo, 661-0974, Japan
Phone: 06-6494-8017  Fax: 
E-mail: yoshiki <at> m.aist.go.jp
home page: http://staff.aist.go.jp/kinoshita.yoshiki/



From: Andreas Abel <andreas.abel <at> ifi.lmu.de>
Subject: [yoshiki] Re: [Agda] Associativity for free!
Date: Fri, 28 Oct 2011 17:26:54 +0200
Message-ID: <4EAAC9BE.9010208 <at> ifi.lmu.de>

andreas.abel> On 10/27/11 3:47 PM, James Chapman wrote:
andreas.abel> > Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
andreas.abel> >
andreas.abel> > Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
andreas.abel> > Y {C} f = λ Z g → comp C g f
andreas.abel> >
andreas.abel> > and we can convert back again:
andreas.abel> >
andreas.abel> > Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
andreas.abel> > Y-1 {C}{A}{B} α = α B (iden C)
andreas.abel> 
andreas.abel> Is that the glorious Yoneda lemma?  Trivial in the language of types. 
andreas.abel> Just subtract the categorical waffle and every programmer understands it...
andreas.abel> 
andreas.abel> Cheers,
andreas.abel> Andreas
andreas.abel> 
andreas.abel> -- 
andreas.abel> Andreas Abel  <><      Du bist der geliebte Mensch.
andreas.abel> 
andreas.abel> Theoretical Computer Science, University of Munich
andreas.abel> Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel> 
andreas.abel> andreas.abel <at> ifi.lmu.de
andreas.abel> http://www2.tcs.ifi.lmu.de/~abel/

andreas.abel> _______________________________________________
andreas.abel> Agda mailing list
andreas.abel> Agda <at> lists.chalmers.se
andreas.abel> https://lists.chalmers.se/mailman/listinfo/agda

andreas.abel> 
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Andreas Abel | 2 Nov 18:48 2011
Picon

Re: [yoshiki] Re: Associativity for free!

Dear Yoshiki,

my colleague Ulrich Schoepp always told me the Yoneda lemma was 
"trivial", meaning "easy", but me being not so fluent in category theory 
usually got lost trying to understand the statement.  However, I can 
read type signatures...

Cheers,
Andreas

On 11/1/11 1:57 PM, KINOSHITA Yoshiki wrote:
> Dear Andreas,
>
> surely, what James described is a part of (gateway to?) Yoneda lemma.
>
> I think you are right in saying that it is trivial.  The whole body of
> Yoneda lemma is trivial.  I recall Peter Freyd wrote something which
> means that many theorems in category theory are trivial, but it is not
> trivial to find a setting which makes those things trivial.  I am sure
> Freyd's original wording was much better.  I once read it in some
> mailing list, was impressed by it, talked about it with several
> people, lost the article and have never found it again.  I miss it...
>
> Yoshiki.
> --
> Yoshiki Kinoshita, D.Sc.
> Principal Research Scientist
> Information Technology Research Insititute
> National Institute of Advanced Industrial Science and Technology (AIST)
> 3-11-46 Nakoji, Amagasaki-shi
> Hyogo, 661-0974, Japan
> Phone: 06-6494-8017  Fax:
> E-mail: yoshiki <at> m.aist.go.jp
> home page: http://staff.aist.go.jp/kinoshita.yoshiki/
>
>
> From: Andreas Abel<andreas.abel@...>
> Subject: [yoshiki] Re: [Agda] Associativity for free!
> Date: Fri, 28 Oct 2011 17:26:54 +0200
> Message-ID:<4EAAC9BE.9010208@...>
>
> andreas.abel>  On 10/27/11 3:47 PM, James Chapman wrote:
> andreas.abel>  >  Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
> andreas.abel>  >
> andreas.abel>  >  Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
> andreas.abel>  >  Y {C} f = λ Z g → comp C g f
> andreas.abel>  >
> andreas.abel>  >  and we can convert back again:
> andreas.abel>  >
> andreas.abel>  >  Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
> andreas.abel>  >  Y-1 {C}{A}{B} α = α B (iden C)
> andreas.abel>
> andreas.abel>  Is that the glorious Yoneda lemma?  Trivial in the language of types.
> andreas.abel>  Just subtract the categorical waffle and every programmer understands it...
> andreas.abel>
> andreas.abel>  Cheers,
> andreas.abel>  Andreas
> andreas.abel>
> andreas.abel>  --
> andreas.abel>  Andreas Abel<><       Du bist der geliebte Mensch.
> andreas.abel>
> andreas.abel>  Theoretical Computer Science, University of Munich
> andreas.abel>  Oettingenstr. 67, D-80538 Munich, GERMANY
> andreas.abel>
> andreas.abel>  andreas.abel@...
> andreas.abel>  http://www2.tcs.ifi.lmu.de/~abel/
> andreas.abel>  _______________________________________________
> andreas.abel>  Agda mailing list
> andreas.abel>  Agda@...
> andreas.abel>  https://lists.chalmers.se/mailman/listinfo/agda
> andreas.abel>

--

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

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

andreas.abel@...
http://www2.tcs.ifi.lmu.de/~abel/
Peter Hancock | 2 Nov 21:12 2011
Picon

Re: [yoshiki] Re: Associativity for free!


> my colleague Ulrich Schoepp always told me the Yoneda lemma was
> "trivial", meaning "easy", but me being not so fluent in category
> theory usually got lost trying to understand the statement. However,
> I can read type signatures...

My supervisor, Robin Gandy, an old-school logician, once said to me
(approximately...): "I've stared at it several times.  Sometimes I feel it is
completely trivial; and at other times I feel it is totally mysterious."

I have to admit I often feel the same about things in category theory.

By the way, for the record, the Yoneda lemma says that the natural transformations
from the functor Hom[A,_] for A : C to some random functor F : C -> Set have
the same cardinal as F(A).  Maybe Andreas can translate that into a type signature?

Hank
KINOSHITA Yoshiki | 3 Nov 02:25 2011
Picon

Re: [yoshiki] Re: Associativity for free!

Dear Anderas,

andreas.abel> my colleague Ulrich Schoepp always told me the Yoneda
andreas.abel> lemma was "trivial", meaning "easy", but me being not so
andreas.abel> fluent in category theory usually got lost trying to
andreas.abel> understand the statement.  However, I can read type
andreas.abel> signatures...

You might be interested in looking at the Agda code for the proof of
Yoneda lemma which I posted after the last AIM.  It is in "Libraries
and other developments" page of Agda wiki.  I have already started to
forget what are in it, but I just checked not only the proposition
attributed to Yoneda in MacLane's book but also the definition of
Yoneda embedding is there.

Yoshiki.
Thorsten Altenkirch | 3 Nov 10:39 2011
Picon

Yoneda was Re: Associativity for free!

On 28 Oct 2011, at 16:26, Andreas Abel wrote:

> On 10/27/11 3:47 PM, James Chapman wrote:
>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>> 
>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>> Y {C} f = λ Z g → comp C g f
>> 
>> and we can convert back again:
>> 
>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>> Y-1 {C}{A}{B} α = α B (iden C)
> 
> Is that the glorious Yoneda lemma?  Trivial in the language of types. Just subtract the categorical waffle
and every programmer understands it...

Indeed, I have been pushing this for a while. Actually given F : Set -> Set a functor, Yoneda just says for any A
: Set:

((X : Set) -> (A -> X) -> F X) ~ F A

where ~ is isomorphism (or equality f we accept univalence). And yes this is a consequence of parametricity
or more precisely of the assumption that (X : Set) -> H X X is a coend (where H : Set^op -> Set -> Set is a bifunctor).

One interesting aspect of this equation is that the left hand side is actually large (in Set_1) while the
right hand side is small. So it is a "resizing axiom" which enables to make big things small.

There are many nice applications of the Yoneda lemma. One of my favourites is the derivation of the
exponential of endofunctors (i.e. the function space in Set -> Set) which is actually a categorical
generalisation of Kripke semantics.

Given F,G : Set -> Set (functors) and exponential F=>G if it exists must satisfy

	((X : Set) -> (H x F) X -> G X) ~ ((X : Set) -> H X -> (F => G) X)		(1)

and it is easy to see that (H x F) X = H X x F X (products are constructed pointwise).

Hence we can calculate

	(F => G) A
	~ (X : Set) (A -> X) -> (F => G) X		(Yoneda)
	~ (X : Set) (A -> X) x F X -> G X			(1)
	~ (X : Set) (A -> X) -> F X -> G X		(currying)

The relation to Kripke semantics becomes clear if we read (A -> X) as X is a future of A. Actually we should
really use the contravariant version then we can read -> as implication.

It is a generalisation because it is an isomorphism as opposed to a logical equivalence.

So, yes, functional programmers should be aware of the Yoneda lemma. Ralph Hinze recently wrote a nice
paper expressing the same sentiment (after I showed him the little proof above).

Obviously, Yoneda is much more general than what I wrote above. As indicated it also works for covariant
functors and there also is a version with SIgma types instead of Pi types.

Cheers,
Thorsten

> 
> Cheers,
> Andreas
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel@...
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
Thorsten Altenkirch | 3 Nov 11:50 2011
Picon

Re: Yoneda was Re: Associativity for free!

P.S. Just remembered that I forgot one thing:

On 3 Nov 2011, at 09:39, Thorsten Altenkirch wrote:

> On 28 Oct 2011, at 16:26, Andreas Abel wrote:
> 
>> On 10/27/11 3:47 PM, James Chapman wrote:
>>> Now, Yoneda's embedding says that we can view morphism in C as the following polymorphic function:
>>> 
>>> Y : ∀{C A B} → Hom C A B → (∀ Z → Hom C B Z → Hom C A Z)
>>> Y {C} f = λ Z g → comp C g f
>>> 
>>> and we can convert back again:
>>> 
>>> Y-1 : ∀{C A B} → (∀ Z → Hom C B Z → Hom C A Z) → Hom C A B
>>> Y-1 {C}{A}{B} α = α B (iden C)
>> 
>> Is that the glorious Yoneda lemma?  Trivial in the language of types. Just subtract the categorical
waffle and every programmer understands it...
> 
> Indeed, I have been pushing this for a while. Actually given F : Set -> Set a functor, Yoneda just says for any
A : Set:
> 
> ((X : Set) -> (A -> X) -> F X) ~ F A
> 
> where ~ is isomorphism (or equality f we accept univalence). And yes this is a consequence of
parametricity or more precisely of the assumption that (X : Set) -> H X X is a coend (where H : Set^op -> Set ->
Set is a bifunctor).
> 
> One interesting aspect of this equation is that the left hand side is actually large (in Set_1) while the
right hand side is small. So it is a "resizing axiom" which enables to make big things small.
> 
> There are many nice applications of the Yoneda lemma. One of my favourites is the derivation of the
exponential of endofunctors (i.e. the function space in Set -> Set) which is actually a categorical
generalisation of Kripke semantics.
> 
> Given F,G : Set -> Set (functors) and exponential F=>G if it exists must satisfy
> 
> 	((X : Set) -> (H x F) X -> G X) ~ ((X : Set) -> H X -> (F => G) X)		(1)
> 
> and it is easy to see that (H x F) X = H X x F X (products are constructed pointwise).
> 
> Hence we can calculate
> 
> 	(F => G) A
> 	~ (X : Set) (A -> X) -> (F => G) X		(Yoneda)
> 	~ (X : Set) (A -> X) x F X -> G X			(1)
> 	~ (X : Set) (A -> X) -> F X -> G X		(currying)
> 
> The relation to Kripke semantics becomes clear if we read (A -> X) as X is a future of A. Actually we should
really use the contravariant version then we can read -> as implication.

Don't forget that I said *if* it exists the exponential looks like this. However, we have no reason to assume
that in general 
(X : Set) (A -> X) -> F X -> G X : Set. It is the case if we assume that F and G are containers (see our CIE paper from
last year). 

> 
> It is a generalisation because it is an isomorphism as opposed to a logical equivalence.
> 
> So, yes, functional programmers should be aware of the Yoneda lemma. Ralph Hinze recently wrote a nice
paper expressing the same sentiment (after I showed him the little proof above).
> 
> Obviously, Yoneda is much more general than what I wrote above. As indicated it also works for covariant
functors and there also is a version with SIgma types instead of Pi types.
> 
> Cheers,
> Thorsten
> 
> 
> 
> 
>> 
>> Cheers,
>> Andreas
>> 
>> -- 
>> Andreas Abel  <><      Du bist der geliebte Mensch.
>> 
>> Theoretical Computer Science, University of Munich
>> Oettingenstr. 67, D-80538 Munich, GERMANY
>> 
>> andreas.abel@...
>> http://www2.tcs.ifi.lmu.de/~abel/
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
Randy Pollack | 26 Oct 23:34 2011
Picon

Re: Associativity for free!

> 2. [...] Another solution I learnt from Conor [...]
>
> data _≤_ {X : Set} : List X → List X → Set where
>  done : [] ≤ []
>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')

I think you will find this approach for weakening (of PTS typing) used
already in Geuvers and Nederhof, JAR 1991 (widely circulated by 1989).
 Following Geuvers and Nederhof, this approach is used in many papers
that mentions weakening of a type system or a logic since that time
(e.g. McKinna/Pollack, Pitts, Urban, ...).

Best,
Randy
---
On Wed, Oct 26, 2011 at 5:01 PM, James Chapman <james@...> wrote:
> Hi Alan,
>
> I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.
>
> 1. A trivial solution for your example is simply to make _++_ associate to the left:
>
> data List (X : Set) : Set where
>  []   : List X
>  _::_ : X → List X → List X
>
> _++_ : ∀{X} → List X → List X → List X
> []        ++ xs' = xs'
> (x :: xs) ++ xs' = x :: (xs ++ xs')
>
> infixl 5 _++_
>
> postulate P : ∀{X} → List X → Set
>
> postulate weakening : ∀ {A} (as bs cs : List A) →
>                      P (as ++ cs) → P (as ++ bs ++ cs)
>
> weaken2 : ∀ {A} (as bs cs ds : List A) →
>   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
> weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p
>
> This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse told
me that in a recent implementation of a dependently typed lambda calculus he defined both versions and
didn't end up needing them both at the same time. Do you need both at the same time?
>
> 2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I
learnt from Conor (exercise 15, his AFP notes
http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it. Instead of giving
weakening this type, give a first order presentation of weakenings (functions from a context to the same
context with more stuff chucked in arbitrary places). For  lists this function space would be the
following inductively defined sublist relation:
>
> data _≤_ {X : Set} : List X → List X → Set where
>  done : [] ≤ []
>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
>
> Then, weakening would be something like:
>
> weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'
>
> By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called
order preserving embeddings) in chapter 4 of my thesis
(http://www.cs.ioc.ee/~james/papers/thesis.pdf ) and it was much more pleasant than using ++ as we did
in our Big-step normalization paper (http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this
chapter was based.
>
> Best wishes,
>
> James
>
>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
James Chapman | 26 Oct 23:45 2011
Picon
Picon

Re: Associativity for free!

Thanks for the references Randy.

I also forgot to say before…

Alan: neat trick!

Best,

James

On Oct 27, 2011, at 12:34 AM, Randy Pollack wrote:

>> 2. [...] Another solution I learnt from Conor [...]
>> 
>> data _≤_ {X : Set} : List X → List X → Set where
>> done : [] ≤ []
>> keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>> skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
> 
> I think you will find this approach for weakening (of PTS typing) used
> already in Geuvers and Nederhof, JAR 1991 (widely circulated by 1989).
> Following Geuvers and Nederhof, this approach is used in many papers
> that mentions weakening of a type system or a logic since that time
> (e.g. McKinna/Pollack, Pitts, Urban, ...).
> 
> Best,
> Randy
> ---
> On Wed, Oct 26, 2011 at 5:01 PM, James Chapman <james@...> wrote:
>> Hi Alan,
>> 
>> I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.
>> 
>> 1. A trivial solution for your example is simply to make _++_ associate to the left:
>> 
>> data List (X : Set) : Set where
>>  []   : List X
>>  _::_ : X → List X → List X
>> 
>> _++_ : ∀{X} → List X → List X → List X
>> []        ++ xs' = xs'
>> (x :: xs) ++ xs' = x :: (xs ++ xs')
>> 
>> infixl 5 _++_
>> 
>> postulate P : ∀{X} → List X → Set
>> 
>> postulate weakening : ∀ {A} (as bs cs : List A) →
>>                      P (as ++ cs) → P (as ++ bs ++ cs)
>> 
>> weaken2 : ∀ {A} (as bs cs ds : List A) →
>>   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
>> weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p
>> 
>> This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse
told me that in a recent implementation of a dependently typed lambda calculus he defined both versions
and didn't end up needing them both at the same time. Do you need both at the same time?
>> 
>> 2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I
learnt from Conor (exercise 15, his AFP notes
http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it. Instead of giving
weakening this type, give a first order presentation of weakenings (functions from a context to the same
context with more stuff chucked in arbitrary places). For  lists this function space would be the
following inductively defined sublist relation:
>> 
>> data _≤_ {X : Set} : List X → List X → Set where
>>  done : [] ≤ []
>>  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
>>  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')
>> 
>> Then, weakening would be something like:
>> 
>> weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'
>> 
>> By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called
order preserving embeddings) in chapter 4 of my thesis
(http://www.cs.ioc.ee/~james/papers/thesis.pdf ) and it was much more pleasant than using ++ as we did
in our Big-step normalization paper (http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this
chapter was based.
>> 
>> Best wishes,
>> 
>> James
>> 
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
>> 
Nils Anders Danielsson | 4 Nov 11:28 2011
Picon
Picon

Re: Associativity for free!

On 2011-10-26 23:01, James Chapman wrote:
> This may sound silly and perhaps you might somewhere else need append
> to associate to the right. Nisse told me that in a recent
> implementation of a dependently typed lambda calculus he defined both
> versions and didn't end up needing them both at the same time.

Contexts:

   data Ctxt : Set where
     ε   : Ctxt
     _▻_ : (Γ : Ctxt) (σ : Type Γ) → Ctxt

Cons-based context extensions:

   data Ctxt₊ (Γ : Ctxt) : Set where
     ε   : Ctxt₊ Γ
     _◅_ : (σ : Type Γ) (Γ₊ : Ctxt₊ (Γ ▻ σ)) → Ctxt₊ Γ

Snoc-based context extensions:

   data Ctxt⁺ (Γ : Ctxt) : Set where
     ε   : Ctxt⁺ Γ
     _▻_ : (Γ⁺ : Ctxt⁺ Γ) (σ : Type (Γ ++⁺ Γ⁺)) → Ctxt⁺ Γ

The cons-based extensions are convenient if you want to define something
like weakening for a Kripke model, because

   (Γ ▻ σ) ++₊ Γ₊

is by definition equal to

   Γ ++₊ (σ ◅ Γ₊).

On the other hand, the snoc-based extensions are convenient if you want
to go under many lambdas, because

   (Γ ++⁺ Γ⁺) ▻ σ

is by definition equal to

   Γ ++⁺ (Γ⁺ ▻ σ).

For more details (work in progress):

   http://www.cse.chalmers.se/~nad/listings/dependently-typed-syntax/README.html
   darcs get http://www.cse.chalmers.se/~nad/repos/dependently-typed-syntax/

--

-- 
/NAD
Nicolas Pouillard | 26 Oct 23:28 2011
Picon

Re: Associativity for free!

On Wed, Oct 26, 2011 at 4:48 PM, Alan Jeffrey <ajeffrey@...> 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?

Well done, nice trick!

I've just tried on natural numbers using difference nats, then vectors based
on these nats and finally associativity of ++ goes well.

module diffnat-assoc where

open import Data.Nat
open import Function
open import Relation.Binary.PropositionalEquality

record D : Set where
  constructor mk
  field
    n    : ℕ
    f     : ℕ → ℕ
    .f✓ : f ≡ _+_ n

_ᴰ : ℕ → D
n ᴰ = mk n (_+_ n) refl

_+ᴰ_ : D → D → D
mk m f f✓ +ᴰ mk n g g✓ = mk (f n) (f ∘ g) (f∘g✓ f f✓ g g✓)
 where
  assoc : ∀ m {n} → (λ x → m + (n + x)) ≡ _+_ (m + n)
  assoc zero    = refl
  assoc (suc m) = cong (_∘_ suc) (assoc m)

  .f∘g✓ : ∀ f (f✓ : f ≡ _+_ m) g (g✓ : g ≡ _+_ n) → f ∘ g ≡ _+_ (f n)
  f∘g✓ ._ refl ._ refl = assoc m

0ᴰ : D
0ᴰ = 0 ᴰ

1ᴰ : D
1ᴰ = 1 ᴰ

sucᴰ : D → D
sucᴰ = _+ᴰ_ 1ᴰ

free-assoc : ∀ {m n o} → m +ᴰ (n +ᴰ o) ≡ (m +ᴰ n) +ᴰ o
free-assoc = refl

data Vec (A : Set) : D → Set where
  [] : Vec A 0ᴰ
  _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (sucᴰ n)

_++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +ᴰ n)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

free-Vec-assoc : ∀ {A m n o} → Vec A ((m +ᴰ n) +ᴰ o) ≡ Vec A (m +ᴰ (n +ᴰ o))
free-Vec-assoc = refl

-- With usual vectors one can't even state this
-- lemma using homogeneous equality.
++-assoc : ∀ {A m n o} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
             (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc []       ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)

--

-- 
Nicolas Pouillard
http://nicolaspouillard.fr
Alan Jeffrey | 27 Oct 02:58 2011

Re: Associativity for free!

Cool! For your next trick, difference vectors over difference naturals, 
and get associativity for free there :-)

A.

On 10/26/2011 04:28 PM, Nicolas Pouillard wrote:
> On Wed, Oct 26, 2011 at 4:48 PM, Alan Jeffrey<ajeffrey@...>  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?
>
> Well done, nice trick!
>
> I've just tried on natural numbers using difference nats, then vectors based
> on these nats and finally associativity of ++ goes well.
>
> module diffnat-assoc where
>
> open import Data.Nat
> open import Function
> open import Relation.Binary.PropositionalEquality
>
> record D : Set where
>    constructor mk
>    field
>      n    : ℕ
>      f     : ℕ → ℕ
>      .f✓ : f ≡ _+_ n
>
> _ᴰ : ℕ → D
> n ᴰ = mk n (_+_ n) refl
>
> _+ᴰ_ : D → D → D
> mk m f f✓ +ᴰ mk n g g✓ = mk (f n) (f ∘ g) (f∘g✓ f f✓ g g✓)
>   where
>    assoc : ∀ m {n} → (λ x → m + (n + x)) ≡ _+_ (m + n)
>    assoc zero    = refl
>    assoc (suc m) = cong (_∘_ suc) (assoc m)
>
>    .f∘g✓ : ∀ f (f✓ : f ≡ _+_ m) g (g✓ : g ≡ _+_ n) → f ∘ g ≡ _+_ (f n)
>    f∘g✓ ._ refl ._ refl = assoc m
>
> 0ᴰ : D
> 0ᴰ = 0 ᴰ
>
> 1ᴰ : D
> 1ᴰ = 1 ᴰ
>
> sucᴰ : D → D
> sucᴰ = _+ᴰ_ 1ᴰ
>
> free-assoc : ∀ {m n o} → m +ᴰ (n +ᴰ o) ≡ (m +ᴰ n) +ᴰ o
> free-assoc = refl
>
> data Vec (A : Set) : D → Set where
>    [] : Vec A 0ᴰ
>    _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (sucᴰ n)
>
> _++_ : ∀ {A m n} → Vec A m → Vec A n → Vec A (m +ᴰ n)
> []       ++ ys = ys
> (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
>
> free-Vec-assoc : ∀ {A m n o} → Vec A ((m +ᴰ n) +ᴰ o) ≡ Vec A (m +ᴰ (n +ᴰ o))
> free-Vec-assoc = refl
>
> -- With usual vectors one can't even state this
> -- lemma using homogeneous equality.
> ++-assoc : ∀ {A m n o} (xs : Vec A m) (ys : Vec A n) (zs : Vec A o) →
>               (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
> ++-assoc []       ys zs = refl
> ++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
>
>
Alan Jeffrey | 2 Nov 17:26 2011

Re: Associativity for free!

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.
Andreas Abel | 2 Nov 18:46 2011
Picon

Re: Re: Associativity for free!

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@...
> 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@...
http://www2.tcs.ifi.lmu.de/~abel/
Alan Jeffrey | 2 Nov 22:10 2011

Re: Re: Associativity for free!

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@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
Andrea Vezzosi | 4 Nov 12:06 2011
Picon

Re: Re: Associativity for free!

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@...> 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@...
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>>
> _______________________________________________
> Agda mailing list
> Agda@...
> https://lists.chalmers.se/mailman/listinfo/agda
>
Alan Jeffrey | 4 Nov 19:07 2011

Re: Re: Associativity for free!

OK, that was very helful, a lot of boilerplate code that was duplicated 
between substitutions and weakening has vanished.

> https://github.com/agda/agda-frp-js/blob/master/src/agda/FRP/JS/Model/STLambdaC/Exp.agda

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@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
James Chapman | 4 Nov 12:29 2011
Picon
Picon

Re: Re: Associativity for free!

Dear Alan + all,

On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey@...> wrote:
> 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.

For contrast, here's renaming and substitution for well typed lambda
terms. Renamings are just functions from variables to variables,
substitutions are just functions form variables to terms. No clever
representations here, no clever getting them both as a instance of a
more general operation, I just wanted to use the interface to
substitution suggested by the (relative) monadic nature of well-typed
terms. The proof is a simplification of the paper proof in Altenkirch
and Reus' paper "Monadic presentations of lambda terms using
generalized inductive types" and follows the approximately the same
structure. The development goes up to proving that the substitution
operation commutes with composition of substitutions (just composition
of functions) -- the third monad law. It's about 170 lines in all
including the utilities prelude.

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
  refl : {a : A} → a ≅ a

trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
trans refl p = p

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≅ g {a}) →
                 _≅_ { {a : A} → B a} { {a : A} → B' a} f g

postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
                (∀ a → f a ≅ g a) → f ≅ g

--Well type lambda terms

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ε   : Con
  _<_ : Con → Ty → Con

data Var : Con → Ty → Set where
  vz : ∀{Γ σ} → Var (Γ < σ) σ
  vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ

renId : ∀{Γ} → Ren Γ Γ
renId = id

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = f • g

wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
wk f vz     = vz
wk f (vs i) = vs (f i)

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
ren f (var x)   = var (f x)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (wk f) t)

wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
wkid vz     = refl
wkid (vs x) = refl

renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
renid (var x)   = refl
renid (app t u) = resp2 app (renid t) (renid u)
renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
                                      (iext (λ _ → ext wkid)))
                                (renid t))

wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
            wk (renComp f g) x ≅ renComp (wk f) (wk g) x
wkcomp f g vz     = refl
wkcomp f g (vs i) = refl

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
            ren (renComp f g) t ≅ (ren f • ren g) t
rencomp f g (var x)   = refl
rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
                                              (iext λ _ → ext (wkcomp f g)))
                                        (rencomp (wk f) (wk g) t))

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ

lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
lift f vz     = var vz
lift f (vs x) = ren vs (f x)

sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
sub f (var x)   = f x
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

subId : ∀{Γ} → Sub Γ Γ
subId = var

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g = sub f • g

liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
liftid vz     = refl
liftid (vs x) = refl

-- first monad law, the second holds definitionally
subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
subid (var x)   = refl
subid (app t u) = resp2 app (subid t) (subid u)
subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
                                        (iext λ _ → ext liftid))
                                  (subid t))

liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
            (lift f • wk g) x ≅ lift (f • g) x
liftwk f g vz     = refl
liftwk f g (vs x) = refl

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
         (sub f • ren g) t ≅ sub (f • g) t
subren f g (var x)   = refl
subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
                                       (resp (λ (f : Sub _ _) → sub f t)
                                             (iext λ _ → ext (liftwk f g))))

renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
               (ren (wk f) • lift g) x ≅ lift (ren f • g) x
renwklift f g vz     = refl
renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
                                (rencomp vs f (g x))

rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
         (ren f •  sub g) t ≅ sub (ren f • g) t
rensub f g (var x)   = refl
rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
                                       (resp (λ (f : Sub _ _) → sub f t)
                                             (iext λ _ →
                                               ext (renwklift f g))))

liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
           lift (subComp f g) x ≅ subComp (lift f) (lift g) x
liftcomp f g vz     = refl
liftcomp f g (vs x) = trans (rensub vs f (g x))
                            (sym (subren (lift f) vs (g x)))

-- third monad law
subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
          sub (subComp f g) t ≅ (sub f • sub g) t
subcomp f g (var x)   = refl
subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
                                              (iext λ _ → ext (liftcomp f g)))
                                        (subcomp (lift f) (lift g) t))

Regards,

James
Nick Benton | 4 Nov 13:14 2011
Picon

RE: Re: Associativity for free!

There's also a tutorial account of this representation, aimed at the working Coqeur, in

N Benton, C-K Hur, A Kennedy and C McBride. Strongly Typed Term Representations in Coq. 
Journal of Automated Reasoning, special issue on Theory and Applications of Abstraction, Substitution
and Naming. 
Published Online March 2011.
http://www.springerlink.com/content/x7l853p43n374336/


  Nick

-----Original Message-----
From: agda-bounces <at> lists.chalmers.se [mailto:agda-bounces <at> lists.chalmers.se] On Behalf Of James Chapman
Sent: 04 November 2011 11:30
To: Alan Jeffrey
Cc: agda list
Subject: Re: [Agda] Re: Associativity for free!

Dear Alan + all,

On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey <at> bell-labs.com> wrote:
> 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.

For contrast, here's renaming and substitution for well typed lambda
terms. Renamings are just functions from variables to variables,
substitutions are just functions form variables to terms. No clever
representations here, no clever getting them both as a instance of a
more general operation, I just wanted to use the interface to
substitution suggested by the (relative) monadic nature of well-typed
terms. The proof is a simplification of the paper proof in Altenkirch
and Reus' paper "Monadic presentations of lambda terms using
generalized inductive types" and follows the approximately the same
structure. The development goes up to proving that the substitution
operation commutes with composition of substitutions (just composition
of functions) -- the third monad law. It's about 170 lines in all
including the utilities prelude.

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
  refl : {a : A} → a ≅ a

trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
trans refl p = p

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
                 (∀ a → f {a} ≅ g {a}) →
                 _≅_ { {a : A} → B a} { {a : A} → B' a} f g

postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
                (∀ a → f a ≅ g a) → f ≅ g

--Well type lambda terms

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty

data Con : Set where
  ε   : Con
  _<_ : Con → Ty → Con

data Var : Con → Ty → Set where
  vz : ∀{Γ σ} → Var (Γ < σ) σ
  vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ

renId : ∀{Γ} → Ren Γ Γ
renId = id

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = f • g

wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
wk f vz     = vz
wk f (vs i) = vs (f i)

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
ren f (var x)   = var (f x)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (wk f) t)

wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
wkid vz     = refl
wkid (vs x) = refl

renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
renid (var x)   = refl
renid (app t u) = resp2 app (renid t) (renid u)
renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
                                      (iext (λ _ → ext wkid)))
                                (renid t))

wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
            wk (renComp f g) x ≅ renComp (wk f) (wk g) x
wkcomp f g vz     = refl
wkcomp f g (vs i) = refl

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
            ren (renComp f g) t ≅ (ren f • ren g) t
rencomp f g (var x)   = refl
rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
                                              (iext λ _ → ext (wkcomp f g)))
                                        (rencomp (wk f) (wk g) t))

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ

lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
lift f vz     = var vz
lift f (vs x) = ren vs (f x)

sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
sub f (var x)   = f x
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

subId : ∀{Γ} → Sub Γ Γ
subId = var

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g = sub f • g

liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
liftid vz     = refl
liftid (vs x) = refl

-- first monad law, the second holds definitionally
subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
subid (var x)   = refl
subid (app t u) = resp2 app (subid t) (subid u)
subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
                                        (iext λ _ → ext liftid))
                                  (subid t))

liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
            (lift f • wk g) x ≅ lift (f • g) x
liftwk f g vz     = refl
liftwk f g (vs x) = refl

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
         (sub f • ren g) t ≅ sub (f • g) t
subren f g (var x)   = refl
subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
                                       (resp (λ (f : Sub _ _) → sub f t)
                                             (iext λ _ → ext (liftwk f g))))

renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
               (ren (wk f) • lift g) x ≅ lift (ren f • g) x
renwklift f g vz     = refl
renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
                                (rencomp vs f (g x))

rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
         (ren f •  sub g) t ≅ sub (ren f • g) t
rensub f g (var x)   = refl
rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
                                       (resp (λ (f : Sub _ _) → sub f t)
                                             (iext λ _ →
                                               ext (renwklift f g))))

liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
           lift (subComp f g) x ≅ subComp (lift f) (lift g) x
liftcomp f g vz     = refl
liftcomp f g (vs x) = trans (rensub vs f (g x))
                            (sym (subren (lift f) vs (g x)))


-- third monad law
subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
          sub (subComp f g) t ≅ (sub f • sub g) t
subcomp f g (var x)   = refl
subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
                                              (iext λ _ → ext (liftcomp f g)))
                                        (subcomp (lift f) (lift g) t))

Regards,

James
_______________________________________________
Agda mailing list
Agda <at> lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda


_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
James Chapman | 4 Nov 14:22 2011
Picon
Picon

Re: Associativity for free!

I should have said this follows the structure of Altenkirch and Reus' proof for untyped terms.

Also, this agda proof is described in the accepted draft paper "Relative Monads formalized"
(http://www.cs.ioc.ee/~james/Publications.html)  which I should really finish, well, today.

James

On Nov 4, 2011, at 1:29 PM, James Chapman wrote:

> Dear Alan + all,
> 
> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey@...> wrote:
>> 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.
> 
> For contrast, here's renaming and substitution for well typed lambda
> terms. Renamings are just functions from variables to variables,
> substitutions are just functions form variables to terms. No clever
> representations here, no clever getting them both as a instance of a
> more general operation, I just wanted to use the interface to
> substitution suggested by the (relative) monadic nature of well-typed
> terms. The proof is a simplification of the paper proof in Altenkirch
> and Reus' paper "Monadic presentations of lambda terms using
> generalized inductive types" and follows the approximately the same
> structure. The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.
> 
> module WellTypedTerms where
> 
> -- Utilities
> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>  refl : {a : A} → a ≅ a
> 
> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
> trans refl p = p
> 
> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
> sym refl = refl
> 
> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
> resp f refl = refl
> 
> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
> ≅ f a' b'
> resp2 f refl refl = refl
> 
> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
> f • g = λ a → f (g a)
> 
> id : {A : Set} → A → A
> id a = a
> 
> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
>                 (∀ a → f {a} ≅ g {a}) →
>                 _≅_ { {a : A} → B a} { {a : A} → B' a} f g
> 
> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>                (∀ a → f a ≅ g a) → f ≅ g
> 
> --Well type lambda terms
> 
> data Ty : Set where
>  ι   : Ty
>  _⇒_ : Ty → Ty → Ty
> 
> data Con : Set where
>  ε   : Con
>  _<_ : Con → Ty → Con
> 
> data Var : Con → Ty → Set where
>  vz : ∀{Γ σ} → Var (Γ < σ) σ
>  vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ
> 
> data Tm : Con → Ty → Set where
>  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)
> 
> -- Renaming
> 
> Ren : Con → Con → Set
> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
> 
> renId : ∀{Γ} → Ren Γ Γ
> renId = id
> 
> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
> renComp f g = f • g
> 
> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
> wk f vz     = vz
> wk f (vs i) = vs (f i)
> 
> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
> ren f (var x)   = var (f x)
> ren f (app t u) = app (ren f t) (ren f u)
> ren f (lam t)   = lam (ren (wk f) t)
> 
> wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
> wkid vz     = refl
> wkid (vs x) = refl
> 
> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
> renid (var x)   = refl
> renid (app t u) = resp2 app (renid t) (renid u)
> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                      (iext (λ _ → ext wkid)))
>                                (renid t))
> 
> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
>            wk (renComp f g) x ≅ renComp (wk f) (wk g) x
> wkcomp f g vz     = refl
> wkcomp f g (vs i) = refl
> 
> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>            ren (renComp f g) t ≅ (ren f • ren g) t
> rencomp f g (var x)   = refl
> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                              (iext λ _ → ext (wkcomp f g)))
>                                        (rencomp (wk f) (wk g) t))
> 
> -- Substitutions
> 
> Sub : Con → Con → Set
> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
> 
> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
> lift f vz     = var vz
> lift f (vs x) = ren vs (f x)
> 
> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
> sub f (var x)   = f x
> sub f (app t u) = app (sub f t) (sub f u)
> sub f (lam t)   = lam (sub (lift f) t)
> 
> subId : ∀{Γ} → Sub Γ Γ
> subId = var
> 
> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
> subComp f g = sub f • g
> 
> liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
> liftid vz     = refl
> liftid (vs x) = refl
> 
> -- first monad law, the second holds definitionally
> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
> subid (var x)   = refl
> subid (app t u) = resp2 app (subid t) (subid u)
> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                        (iext λ _ → ext liftid))
>                                  (subid t))
> 
> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
>            (lift f • wk g) x ≅ lift (f • g) x
> liftwk f g vz     = refl
> liftwk f g (vs x) = refl
> 
> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>         (sub f • ren g) t ≅ sub (f • g) t
> subren f g (var x)   = refl
> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>                                       (resp (λ (f : Sub _ _) → sub f t)
>                                             (iext λ _ → ext (liftwk f g))))
> 
> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
>               (ren (wk f) • lift g) x ≅ lift (ren f • g) x
> renwklift f g vz     = refl
> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>                                (rencomp vs f (g x))
> 
> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>         (ren f •  sub g) t ≅ sub (ren f • g) t
> rensub f g (var x)   = refl
> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>                                       (resp (λ (f : Sub _ _) → sub f t)
>                                             (iext λ _ →
>                                               ext (renwklift f g))))
> 
> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
>           lift (subComp f g) x ≅ subComp (lift f) (lift g) x
> liftcomp f g vz     = refl
> liftcomp f g (vs x) = trans (rensub vs f (g x))
>                            (sym (subren (lift f) vs (g x)))
> 
> 
> -- third monad law
> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>          sub (subComp f g) t ≅ (sub f • sub g) t
> subcomp f g (var x)   = refl
> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                              (iext λ _ → ext (liftcomp f g)))
>                                        (subcomp (lift f) (lift g) t))
> 
> Regards,
> 
> James
Andrea Vezzosi | 4 Nov 14:42 2011
Picon

Re: Re: Associativity for free!

On Fri, Nov 4, 2011 at 12:29 PM, James Chapman <james@...> wrote:
> [...] The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.

And yet, even without fancy representations, it can be trimmed down to
109 lines and many less intermediate constructions by working under a
context:

module WellTypedTerms where

-- Utilities
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
 refl : {a : A} → a ≅ a

trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
trans refl p = p

sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
sym refl = refl

resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B x) → C x y)
          {a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b ≅ f a' b'
resp2 f refl refl = refl

_•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
     (∀ {a} b → C a b) → (g : (∀ (a : A) → B a)) → ∀ (a : A) → C a (g a)
f • g = λ a → f (g a)

id : {A : Set} → A → A
id a = a

--Well type lambda terms

data Ty : Set where
 ι   : Ty
 _⇒_ : Ty → Ty → Ty

data Con : Set where
 ε   : Con
 _<_ : Con → Ty → Con

_<<_ : Con -> Con -> Con
Γ << ε = Γ
Γ << (Δ < τ) = (Γ << Δ) < τ

data Var : Con → Ty → Set where
 vz : ∀{Γ σ} → Var (Γ < σ) σ
 vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ

data Tm : Con → Ty → Set where
 var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
 app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
 lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)

-- Substitutions

Sub : Con → Con → Set
Sub Γ Δ = ∀ K {σ} → Var (Γ << K) σ → Tm (Δ << K) σ

sub : ∀{Γ Δ} → Sub Γ Δ → ∀ K {σ} → Tm (Γ << K) σ → Tm (Δ << K) σ
sub f K (var x)   = f K x
sub f K (app t u) = app (sub f K t) (sub f K u)
sub f K (lam t)   = lam (sub f (K < _) t)

subId : ∀{Γ} → Sub Γ Γ
subId = λ K x -> var x

subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
subComp f g K = sub f K • g K

-- first monad law, the second holds definitionally
subid : ∀{Γ}K{σ}(t : Tm (Γ << K) σ) → sub subId K t ≅ id t
subid K (var x)   = refl
subid K (app t u) = resp2 app (subid K t) (subid K u)
subid K (lam t)   = resp lam (subid (K < _) t)

-- Renaming

Ren : Con → Con → Set
Ren Γ Δ = ∀ K {σ} → Var (Γ << K) σ → Var (Δ << K) σ

renId : ∀{Γ} → Ren Γ Γ
renId = \ _ x -> x

renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
renComp f g = \ K -> f K • g K

ren : ∀{Γ Δ} → Ren Γ Δ → ∀ K {σ} → Tm (Γ << K) σ → Tm (Δ << K) σ
ren f K x = sub (λ K → subId K • f K) K x

renid : ∀{Γ} K {σ}(t : Tm (Γ << K) σ) → ren renId K t ≅ id t
renid = subid

rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ) K {σ}(t : Tm (B << K) σ) →
           ren (renComp f g) K t ≅ (ren f K • ren g K) t
rencomp f g K (var x)   = refl
rencomp f g K (app t u) = resp2 app (rencomp f g K t) (rencomp f g K u)
rencomp {B}{Γ}{Δ} f g K (lam t) = resp lam (rencomp f g (K < _) t)

-- third monad law
subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ)K{σ}(t : Tm (B << K) σ) →
         sub (subComp f g) K t ≅ (sub f K • sub g K) t
subcomp f g K (var x)   = refl
subcomp f g K (app t u) = resp2 app (subcomp f g K t) (subcomp f g K u)
subcomp f g K (lam t)   = resp lam (subcomp f g (K < _) t)

-- these are now corollaries
rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ)K{σ}(t : Tm (B << K) σ) →
        (ren f K • sub g K) t ≅ sub (λ K -> ren f K • g K) K t
rensub f g K t = sym (subcomp (λ K → subId K • f K) g K t)

subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ)K{σ}(t : Tm (B << K) σ) →
        (sub f K • ren g K) t ≅ sub (λ K -> f K • g K) K t
subren f g K x = sym (subcomp f (λ K' → subId K' • g K') K x)
James Chapman | 4 Nov 15:18 2011
Picon
Picon

Re: Re: Associativity for free!

On Nov 4, 2011, at 3:42 PM, Andrea Vezzosi wrote:
> On Fri, Nov 4, 2011 at 12:29 PM, James Chapman <james@...> wrote:
> And yet, even without fancy representations, it can be trimmed down to
> 109 lines and many less intermediate constructions by working under a
> context:

Neat! Thanks, perhaps I should post my code to the agda list more often ;)

James
Alan Jeffrey | 4 Nov 18:55 2011

Re: Re: Associativity for free!

OK, that's pretty cool. The nasty case which hit me was proving 
properties like "weakening of weakening is weakening":

   weaken* A (weaken* B M) ≡ weaken* (A ++ B) M

which you can't even state without putting in some explicit associators.

This came up in the context of normalization by evaluation, which needs 
a Kripke-like structure which extends the context on every function 
application. Associators were really getting in the way, as I was 
needing to prove a bunch of coherence properties. Have you tried getting 
an NBE proof to go through in your setting?

A.

On 11/04/2011 06:29 AM, James Chapman wrote:
> Dear Alan + all,
>
> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey<ajeffrey@...>  wrote:
>> 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.
>
> For contrast, here's renaming and substitution for well typed lambda
> terms. Renamings are just functions from variables to variables,
> substitutions are just functions form variables to terms. No clever
> representations here, no clever getting them both as a instance of a
> more general operation, I just wanted to use the interface to
> substitution suggested by the (relative) monadic nature of well-typed
> terms. The proof is a simplification of the paper proof in Altenkirch
> and Reus' paper "Monadic presentations of lambda terms using
> generalized inductive types" and follows the approximately the same
> structure. The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.
>
> module WellTypedTerms where
>
> -- Utilities
> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>    refl : {a : A} → a ≅ a
>
> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
> trans refl p = p
>
> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
> sym refl = refl
>
> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
> resp f refl = refl
>
> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
> ≅ f a' b'
> resp2 f refl refl = refl
>
> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>        (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
> f • g = λ a → f (g a)
>
> id : {A : Set} → A → A
> id a = a
>
> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
>                   (∀ a → f {a} ≅ g {a}) →
>                   _≅_ { {a : A} → B a} { {a : A} → B' a} f g
>
> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>                  (∀ a → f a ≅ g a) → f ≅ g
>
> --Well type lambda terms
>
> data Ty : Set where
>    ι   : Ty
>    _⇒_ : Ty → Ty → Ty
>
> data Con : Set where
>    ε   : Con
>    _<_ : Con → Ty → Con
>
> data Var : Con → Ty → Set where
>    vz : ∀{Γ σ} → Var (Γ<  σ) σ
>    vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ<  τ) σ
>
> data Tm : Con → Ty → Set where
>    var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>    app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>    lam : ∀{Γ σ τ} → Tm (Γ<  σ) τ → Tm Γ (σ ⇒ τ)
>
> -- Renaming
>
> Ren : Con → Con → Set
> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>
> renId : ∀{Γ} → Ren Γ Γ
> renId = id
>
> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
> renComp f g = f • g
>
> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ<  σ) (Δ<  σ)
> wk f vz     = vz
> wk f (vs i) = vs (f i)
>
> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
> ren f (var x)   = var (f x)
> ren f (app t u) = app (ren f t) (ren f u)
> ren f (lam t)   = lam (ren (wk f) t)
>
> wkid : ∀{Γ σ τ}(x : Var (Γ<  τ) σ) → wk renId x ≅ renId x
> wkid vz     = refl
> wkid (vs x) = refl
>
> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
> renid (var x)   = refl
> renid (app t u) = resp2 app (renid t) (renid u)
> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                        (iext (λ _ → ext wkid)))
>                                  (renid t))
>
> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>              wk (renComp f g) x ≅ renComp (wk f) (wk g) x
> wkcomp f g vz     = refl
> wkcomp f g (vs i) = refl
>
> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>              ren (renComp f g) t ≅ (ren f • ren g) t
> rencomp f g (var x)   = refl
> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                                (iext λ _ → ext (wkcomp f g)))
>                                          (rencomp (wk f) (wk g) t))
>
> -- Substitutions
>
> Sub : Con → Con → Set
> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>
> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ<  σ) (Δ<  σ)
> lift f vz     = var vz
> lift f (vs x) = ren vs (f x)
>
> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
> sub f (var x)   = f x
> sub f (app t u) = app (sub f t) (sub f u)
> sub f (lam t)   = lam (sub (lift f) t)
>
> subId : ∀{Γ} → Sub Γ Γ
> subId = var
>
> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
> subComp f g = sub f • g
>
> liftid : ∀{Γ σ τ}(x : Var (Γ<  σ) τ) → lift subId x ≅ subId x
> liftid vz     = refl
> liftid (vs x) = refl
>
> -- first monad law, the second holds definitionally
> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
> subid (var x)   = refl
> subid (app t u) = resp2 app (subid t) (subid u)
> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                          (iext λ _ → ext liftid))
>                                    (subid t))
>
> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>              (lift f • wk g) x ≅ lift (f • g) x
> liftwk f g vz     = refl
> liftwk f g (vs x) = refl
>
> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>           (sub f • ren g) t ≅ sub (f • g) t
> subren f g (var x)   = refl
> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>                                         (resp (λ (f : Sub _ _) → sub f t)
>                                               (iext λ _ → ext (liftwk f g))))
>
> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>                 (ren (wk f) • lift g) x ≅ lift (ren f • g) x
> renwklift f g vz     = refl
> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>                                  (rencomp vs f (g x))
>
> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>           (ren f •  sub g) t ≅ sub (ren f • g) t
> rensub f g (var x)   = refl
> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>                                         (resp (λ (f : Sub _ _) → sub f t)
>                                               (iext λ _ →
>                                                 ext (renwklift f g))))
>
> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>             lift (subComp f g) x ≅ subComp (lift f) (lift g) x
> liftcomp f g vz     = refl
> liftcomp f g (vs x) = trans (rensub vs f (g x))
>                              (sym (subren (lift f) vs (g x)))
>
>
> -- third monad law
> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>            sub (subComp f g) t ≅ (sub f • sub g) t
> subcomp f g (var x)   = refl
> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                                (iext λ _ → ext (liftcomp f g)))
>                                          (subcomp (lift f) (lift g) t))
>
> Regards,
>
> James
Nils Anders Danielsson | 4 Nov 19:15 2011
Picon
Picon

Re: Re: Associativity for free!

On 2011-11-04 18:55, Alan Jeffrey wrote:
> This came up in the context of normalization by evaluation, which needs
> a Kripke-like structure which extends the context on every function
> application. Associators were really getting in the way, as I was
> needing to prove a bunch of coherence properties. Have you tried getting
> an NBE proof to go through in your setting?

I don't know about James' setting, but I've implemented something close
to NBE [*] in a well-typed way for a dependently typed object language,
and didn't have any problems with associativity (once I found the right
definitions):

    http://www.cse.chalmers.se/~nad/listings/dependently-typed-syntax/README.html

The key trick to avoid problems with associativity was to use cons-based
context extensions.

[*] I didn't prove uniqueness of normal forms, but rather its negation
(almost).

--

-- 
/NAD
Alan Jeffrey | 5 Nov 02:58 2011

Re: Re: Associativity for free!

Yes, it may be that if I'd found the right collection of cons- vs- 
snoc-lists I'd have been able to get NBE to go through without 
associators. At this point, using difference lists around allows me to 
be sloppy about associativity, and have it all magically go through.

So far the main annoyances with difference lists I've found are:

a) Huge normal forms for terms, which tend to bog Agda down, especially 
in proofs with lots of holes.

b) A side-effect of (a) is that error messages or anything else which 
prints a normal form aren't much use, which makes proving properties a 
bit error-prone.

c) There are some unifications on difference lists that Agda fails to 
make, the most annoying of which is unifying (a ∷ as) with (b ∷ bs) 
doesn't unify a with b or as with bs, which is something weird to do 
with unification happening under lambdas.

You pays your money and you takes your choice.

A.

On 11/04/2011 01:15 PM, Nils Anders Danielsson wrote:
> On 2011-11-04 18:55, Alan Jeffrey wrote:
>> This came up in the context of normalization by evaluation, which needs
>> a Kripke-like structure which extends the context on every function
>> application. Associators were really getting in the way, as I was
>> needing to prove a bunch of coherence properties. Have you tried getting
>> an NBE proof to go through in your setting?
>
> I don't know about James' setting, but I've implemented something close
> to NBE [*] in a well-typed way for a dependently typed object language,
> and didn't have any problems with associativity (once I found the right
> definitions):
>
>      http://www.cse.chalmers.se/~nad/listings/dependently-typed-syntax/README.html
>
> The key trick to avoid problems with associativity was to use cons-based
> context extensions.
>
> [*] I didn't prove uniqueness of normal forms, but rather its negation
> (almost).
>
James Chapman | 5 Nov 11:47 2011
Picon
Picon

Re: Re: Associativity for free!

I haven't tried an NBE proof with the version of renaming and
substitution I posted yesterday. I have done something similar during
my PhD. I used OPEs in the end (which I described early in this thread
and Randy pointed to copious prior art).

data OPE : Con -> Con -> Set where
  done : OPE ε ε
  keep : forall {Γ Δ} σ -> OPE Γ Δ -> OPE (Γ < σ) (Δ < σ)
  skip : forall {Γ Δ} σ -> OPE Γ Δ -> OPE (Γ < σ) Δ

I had exactly this problem as you, for me it was with kripke logical
predicates. Instead of defining the kripke-like part as saying:

/a strongly computable function is one that given an strongly
computable  argument in an extended context, and after weakening the
function so that it is in the same context, will give a strongly
computable result./

I defined it using the kripke like bit of strong computability roughly
as follows:

SCV : forall {Γ σ} -> Val Γ σ -> Set
SCV {Γ} {σ ⇒ τ} v       = forall {B}(f : OPE B Γ)(a : Val B σ) -> SCV a ->
  SCV  {B} {τ} (oapp f v $$ a)
SCV ...

i.e. /a strongly computable function is one that given a strongly
computable argument in an arbitrary context B, and a order preserving
embedding from the functions context Γ into B, and after applying the
embedding to the function, we get a strongly computable result./

The context B is arbitrary but OPE Γ B is only inhabited if B is
'larger'. applying oapp twice (composing them) doesn't lead to the
same problem as your weaken as the source and target contexts are just
variables, just like composing functions. OPEs are exactly the
renamings which don't shrink the context and hence useful here.

Regards,

James

On Fri, Nov 4, 2011 at 7:55 PM, Alan Jeffrey <ajeffrey <at> bell-labs.com> wrote:
> OK, that's pretty cool. The nasty case which hit me was proving properties
> like "weakening of weakening is weakening":
>
>  weaken* A (weaken* B M) ≡ weaken* (A ++ B) M
>
> which you can't even state without putting in some explicit associators.
>
> This came up in the context of normalization by evaluation, which needs a
> Kripke-like structure which extends the context on every function
> application. Associators were really getting in the way, as I was needing to
> prove a bunch of coherence properties. Have you tried getting an NBE proof
> to go through in your setting?
>
> A.
>
> On 11/04/2011 06:29 AM, James Chapman wrote:
>>
>> Dear Alan + all,
>>
>> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey<ajeffrey <at> bell-labs.com>
>>  wrote:
>>>
>>> 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.
>>
>> For contrast, here's renaming and substitution for well typed lambda
>> terms. Renamings are just functions from variables to variables,
>> substitutions are just functions form variables to terms. No clever
>> representations here, no clever getting them both as a instance of a
>> more general operation, I just wanted to use the interface to
>> substitution suggested by the (relative) monadic nature of well-typed
>> terms. The proof is a simplification of the paper proof in Altenkirch
>> and Reus' paper "Monadic presentations of lambda terms using
>> generalized inductive types" and follows the approximately the same
>> structure. The development goes up to proving that the substitution
>> operation commutes with composition of substitutions (just composition
>> of functions) -- the third monad law. It's about 170 lines in all
>> including the utilities prelude.
>>
>> module WellTypedTerms where
>>
>> -- Utilities
>> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>>   refl : {a : A} → a ≅ a
>>
>> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅
>> a''
>> trans refl p = p
>>
>> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
>> sym refl = refl
>>
>> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
>> resp f refl = refl
>>
>> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
>> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
>> ≅ f a' b'
>> resp2 f refl refl = refl
>>
>> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>>       (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
>> f • g = λ a → f (g a)
>>
>> id : {A : Set} → A → A
>> id a = a
>>
>> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B'
>> a} →
>>                  (∀ a → f {a} ≅ g {a}) →
>>                  _≅_ { {a : A} → B a} { {a : A} → B' a} f g
>>
>> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>>                 (∀ a → f a ≅ g a) → f ≅ g
>>
>> --Well type lambda terms
>>
>> data Ty : Set where
>>   ι   : Ty
>>   _⇒_ : Ty → Ty → Ty
>>
>> data Con : Set where
>>   ε   : Con
>>   _<_ : Con → Ty → Con
>>
>> data Var : Con → Ty → Set where
>>   vz : ∀{Γ σ} → Var (Γ<  σ) σ
>>   vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ<  τ) σ
>>
>> data Tm : Con → Ty → Set where
>>   var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>>   app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>>   lam : ∀{Γ σ τ} → Tm (Γ<  σ) τ → Tm Γ (σ ⇒ τ)
>>
>> -- Renaming
>>
>> Ren : Con → Con → Set
>> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>>
>> renId : ∀{Γ} → Ren Γ Γ
>> renId = id
>>
>> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
>> renComp f g = f • g
>>
>> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ<  σ) (Δ<  σ)
>> wk f vz     = vz
>> wk f (vs i) = vs (f i)
>>
>> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
>> ren f (var x)   = var (f x)
>> ren f (app t u) = app (ren f t) (ren f u)
>> ren f (lam t)   = lam (ren (wk f) t)
>>
>> wkid : ∀{Γ σ τ}(x : Var (Γ<  τ) σ) → wk renId x ≅ renId x
>> wkid vz     = refl
>> wkid (vs x) = refl
>>
>> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
>> renid (var x)   = refl
>> renid (app t u) = resp2 app (renid t) (renid u)
>> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>                                       (iext (λ _ → ext wkid)))
>>                                 (renid t))
>>
>> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>>             wk (renComp f g) x ≅ renComp (wk f) (wk g) x
>> wkcomp f g vz     = refl
>> wkcomp f g (vs i) = refl
>>
>> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>             ren (renComp f g) t ≅ (ren f • ren g) t
>> rencomp f g (var x)   = refl
>> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
>> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>                                               (iext λ _ → ext (wkcomp f
>> g)))
>>                                         (rencomp (wk f) (wk g) t))
>>
>> -- Substitutions
>>
>> Sub : Con → Con → Set
>> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>>
>> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ<  σ) (Δ<  σ)
>> lift f vz     = var vz
>> lift f (vs x) = ren vs (f x)
>>
>> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
>> sub f (var x)   = f x
>> sub f (app t u) = app (sub f t) (sub f u)
>> sub f (lam t)   = lam (sub (lift f) t)
>>
>> subId : ∀{Γ} → Sub Γ Γ
>> subId = var
>>
>> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
>> subComp f g = sub f • g
>>
>> liftid : ∀{Γ σ τ}(x : Var (Γ<  σ) τ) → lift subId x ≅ subId x
>> liftid vz     = refl
>> liftid (vs x) = refl
>>
>> -- first monad law, the second holds definitionally
>> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
>> subid (var x)   = refl
>> subid (app t u) = resp2 app (subid t) (subid u)
>> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>                                         (iext λ _ → ext liftid))
>>                                   (subid t))
>>
>> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<  σ) τ) →
>>             (lift f • wk g) x ≅ lift (f • g) x
>> liftwk f g vz     = refl
>> liftwk f g (vs x) = refl
>>
>> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>          (sub f • ren g) t ≅ sub (f • g) t
>> subren f g (var x)   = refl
>> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
>> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>>                                        (resp (λ (f : Sub _ _) → sub f t)
>>                                              (iext λ _ → ext (liftwk f
>> g))))
>>
>> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>>                (ren (wk f) • lift g) x ≅ lift (ren f • g) x
>> renwklift f g vz     = refl
>> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>>                                 (rencomp vs f (g x))
>>
>> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>          (ren f •  sub g) t ≅ sub (ren f • g) t
>> rensub f g (var x)   = refl
>> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
>> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>>                                        (resp (λ (f : Sub _ _) → sub f t)
>>                                              (iext λ _ →
>>                                                ext (renwklift f g))))
>>
>> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<  σ) τ) →
>>            lift (subComp f g) x ≅ subComp (lift f) (lift g) x
>> liftcomp f g vz     = refl
>> liftcomp f g (vs x) = trans (rensub vs f (g x))
>>                             (sym (subren (lift f) vs (g x)))
>>
>>
>> -- third monad law
>> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>           sub (subComp f g) t ≅ (sub f • sub g) t
>> subcomp f g (var x)   = refl
>> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
>> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>                                               (iext λ _ → ext (liftcomp f
>> g)))
>>                                         (subcomp (lift f) (lift g) t))
>>
>> Regards,
>>
>> James
>
_______________________________________________
Agda mailing list
Agda@...
https://lists.chalmers.se/mailman/listinfo/agda
Alan Jeffrey | 5 Nov 20:14 2011

Re: Re: Associativity for free!

Fair enough, if you phrase the Kripke structure in terms of subcontext 
inclusion rather than context extension, then I can see how it goes 
through without worrying about associativity.

A.

On 11/05/2011 05:47 AM, James Chapman wrote:
> I haven't tried an NBE proof with the version of renaming and
> substitution I posted yesterday. I have done something similar during
> my PhD. I used OPEs in the end (which I described early in this thread
> and Randy pointed to copious prior art).
>
> data OPE : Con ->  Con ->  Set where
>    done : OPE ε ε
>    keep : forall {Γ Δ} σ ->  OPE Γ Δ ->  OPE (Γ<  σ) (Δ<  σ)
>    skip : forall {Γ Δ} σ ->  OPE Γ Δ ->  OPE (Γ<  σ) Δ
>
> I had exactly this problem as you, for me it was with kripke logical
> predicates. Instead of defining the kripke-like part as saying:
>
> /a strongly computable function is one that given an strongly
> computable  argument in an extended context, and after weakening the
> function so that it is in the same context, will give a strongly
> computable result./
>
> I defined it using the kripke like bit of strong computability roughly
> as follows:
>
> SCV : forall {Γ σ} ->  Val Γ σ ->  Set
> SCV {Γ} {σ ⇒ τ} v       = forall {B}(f : OPE B Γ)(a : Val B σ) ->  SCV a ->
>    SCV  {B} {τ} (oapp f v $$ a)
> SCV ...
>
> i.e. /a strongly computable function is one that given a strongly
> computable argument in an arbitrary context B, and a order preserving
> embedding from the functions context Γ into B, and after applying the
> embedding to the function, we get a strongly computable result./
>
> The context B is arbitrary but OPE Γ B is only inhabited if B is
> 'larger'. applying oapp twice (composing them) doesn't lead to the
> same problem as your weaken as the source and target contexts are just
> variables, just like composing functions. OPEs are exactly the
> renamings which don't shrink the context and hence useful here.
>
> Regards,
>
> James
>
> On Fri, Nov 4, 2011 at 7:55 PM, Alan Jeffrey<ajeffrey@...>  wrote:
>> OK, that's pretty cool. The nasty case which hit me was proving properties
>> like "weakening of weakening is weakening":
>>
>>   weaken* A (weaken* B M) ≡ weaken* (A ++ B) M
>>
>> which you can't even state without putting in some explicit associators.
>>
>> This came up in the context of normalization by evaluation, which needs a
>> Kripke-like structure which extends the context on every function
>> application. Associators were really getting in the way, as I was needing to
>> prove a bunch of coherence properties. Have you tried getting an NBE proof
>> to go through in your setting?
>>
>> A.
>>
>> On 11/04/2011 06:29 AM, James Chapman wrote:
>>>
>>> Dear Alan + all,
>>>
>>> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey<ajeffrey@...>
>>>   wrote:
>>>>
>>>> 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.
>>>
>>> For contrast, here's renaming and substitution for well typed lambda
>>> terms. Renamings are just functions from variables to variables,
>>> substitutions are just functions form variables to terms. No clever
>>> representations here, no clever getting them both as a instance of a
>>> more general operation, I just wanted to use the interface to
>>> substitution suggested by the (relative) monadic nature of well-typed
>>> terms. The proof is a simplification of the paper proof in Altenkirch
>>> and Reus' paper "Monadic presentations of lambda terms using
>>> generalized inductive types" and follows the approximately the same
>>> structure. The development goes up to proving that the substitution
>>> operation commutes with composition of substitutions (just composition
>>> of functions) -- the third monad law. It's about 170 lines in all
>>> including the utilities prelude.
>>>
>>> module WellTypedTerms where
>>>
>>> -- Utilities
>>> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>>>    refl : {a : A} → a ≅ a
>>>
>>> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅
>>> a''
>>> trans refl p = p
>>>
>>> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
>>> sym refl = refl
>>>
>>> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
>>> resp f refl = refl
>>>
>>> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
>>> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
>>> ≅ f a' b'
>>> resp2 f refl refl = refl
>>>
>>> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>>>        (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
>>> f • g = λ a → f (g a)
>>>
>>> id : {A : Set} → A → A
>>> id a = a
>>>
>>> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B'
>>> a} →
>>>                   (∀ a → f {a} ≅ g {a}) →
>>>                   _≅_ { {a : A} → B a} { {a : A} → B' a} f g
>>>
>>> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>>>                  (∀ a → f a ≅ g a) → f ≅ g
>>>
>>> --Well type lambda terms
>>>
>>> data Ty : Set where
>>>    ι   : Ty
>>>    _⇒_ : Ty → Ty → Ty
>>>
>>> data Con : Set where
>>>    ε   : Con
>>>    _<_ : Con → Ty → Con
>>>
>>> data Var : Con → Ty → Set where
>>>    vz : ∀{Γ σ} → Var (Γ<    σ) σ
>>>    vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ<    τ) σ
>>>
>>> data Tm : Con → Ty → Set where
>>>    var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>>>    app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>>>    lam : ∀{Γ σ τ} → Tm (Γ<    σ) τ → Tm Γ (σ ⇒ τ)
>>>
>>> -- Renaming
>>>
>>> Ren : Con → Con → Set
>>> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
>>>
>>> renId : ∀{Γ} → Ren Γ Γ
>>> renId = id
>>>
>>> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
>>> renComp f g = f • g
>>>
>>> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ<    σ) (Δ<    σ)
>>> wk f vz     = vz
>>> wk f (vs i) = vs (f i)
>>>
>>> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
>>> ren f (var x)   = var (f x)
>>> ren f (app t u) = app (ren f t) (ren f u)
>>> ren f (lam t)   = lam (ren (wk f) t)
>>>
>>> wkid : ∀{Γ σ τ}(x : Var (Γ<    τ) σ) → wk renId x ≅ renId x
>>> wkid vz     = refl
>>> wkid (vs x) = refl
>>>
>>> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
>>> renid (var x)   = refl
>>> renid (app t u) = resp2 app (renid t) (renid u)
>>> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>>                                        (iext (λ _ → ext wkid)))
>>>                                  (renid t))
>>>
>>> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>              wk (renComp f g) x ≅ renComp (wk f) (wk g) x
>>> wkcomp f g vz     = refl
>>> wkcomp f g (vs i) = refl
>>>
>>> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>>              ren (renComp f g) t ≅ (ren f • ren g) t
>>> rencomp f g (var x)   = refl
>>> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
>>> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>>>                                                (iext λ _ → ext (wkcomp f
>>> g)))
>>>                                          (rencomp (wk f) (wk g) t))
>>>
>>> -- Substitutions
>>>
>>> Sub : Con → Con → Set
>>> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
>>>
>>> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ<    σ) (Δ<    σ)
>>> lift f vz     = var vz
>>> lift f (vs x) = ren vs (f x)
>>>
>>> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
>>> sub f (var x)   = f x
>>> sub f (app t u) = app (sub f t) (sub f u)
>>> sub f (lam t)   = lam (sub (lift f) t)
>>>
>>> subId : ∀{Γ} → Sub Γ Γ
>>> subId = var
>>>
>>> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
>>> subComp f g = sub f • g
>>>
>>> liftid : ∀{Γ σ τ}(x : Var (Γ<    σ) τ) → lift subId x ≅ subId x
>>> liftid vz     = refl
>>> liftid (vs x) = refl
>>>
>>> -- first monad law, the second holds definitionally
>>> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
>>> subid (var x)   = refl
>>> subid (app t u) = resp2 app (subid t) (subid u)
>>> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>>                                          (iext λ _ → ext liftid))
>>>                                    (subid t))
>>>
>>> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>              (lift f • wk g) x ≅ lift (f • g) x
>>> liftwk f g vz     = refl
>>> liftwk f g (vs x) = refl
>>>
>>> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>>>           (sub f • ren g) t ≅ sub (f • g) t
>>> subren f g (var x)   = refl
>>> subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
>>> subren f g (lam t)   = resp lam (trans (subren (lift f) (wk g) t)
>>>                                         (resp (λ (f : Sub _ _) → sub f t)
>>>                                               (iext λ _ → ext (liftwk f
>>> g))))
>>>
>>> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>                 (ren (wk f) • lift g) x ≅ lift (ren f • g) x
>>> renwklift f g vz     = refl
>>> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>>>                                  (rencomp vs f (g x))
>>>
>>> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>>           (ren f •  sub g) t ≅ sub (ren f • g) t
>>> rensub f g (var x)   = refl
>>> rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
>>> rensub f g (lam t)   = resp lam (trans (rensub (wk f) (lift g) t)
>>>                                         (resp (λ (f : Sub _ _) → sub f t)
>>>                                               (iext λ _ →
>>>                                                 ext (renwklift f g))))
>>>
>>> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B<    σ) τ) →
>>>             lift (subComp f g) x ≅ subComp (lift f) (lift g) x
>>> liftcomp f g vz     = refl
>>> liftcomp f g (vs x) = trans (rensub vs f (g x))
>>>                              (sym (subren (lift f) vs (g x)))
>>>
>>>
>>> -- third monad law
>>> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>>>            sub (subComp f g) t ≅ (sub f • sub g) t
>>> subcomp f g (var x)   = refl
>>> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
>>> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>>>                                                (iext λ _ → ext (liftcomp f
>>> g)))
>>>                                          (subcomp (lift f) (lift g) t))
>>>
>>> Regards,
>>>
>>> James
>>
Andrea Vezzosi | 6 Nov 20:14 2011
Picon

Re: Re: Associativity for free!

On Sat, Nov 5, 2011 at 8:14 PM, Alan Jeffrey <ajeffrey@...> wrote:
> Fair enough, if you phrase the Kripke structure in terms of subcontext
> inclusion rather than context extension, then I can see how it goes through
> without worrying about associativity.

Exactly, and arbitrary renamings seem to do the work here (scroll to
the bottom):
 http://code.haskell.org/~Saizan/WellTypedTerms.agda
Alan Jeffrey | 21 Nov 20:17 2011

Re: Associativity for free!

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.
Andreas Abel | 22 Mar 15:40 2012
Picon

Re: Re: Associativity for free!

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@...
> 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@...
http://www2.tcs.ifi.lmu.de/~abel/
Alan Jeffrey | 22 Mar 15:47 2012

Re: Re: Associativity for free!

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@...
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
Andreas Abel | 22 Mar 17:22 2012
Picon

Re: Re: Associativity for free!

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@...
>>> 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@...
http://www2.tcs.ifi.lmu.de/~abel/
Alan Jeffrey | 22 Mar 17:30 2012

Re: Re: Associativity for free!

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@...
>>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>>
>>>
>>
>
Nils Anders Danielsson | 4 Nov 11:48 2011
Picon
Picon

Re: Associativity for free!

On 2011-10-26 16:48, Alan Jeffrey wrote:
> 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?

I've used the two tricks independently, but I haven't seen them used
together.

One of the tricks (old code, hence Set1, forall and -> rather than Set₁,
∀ and →):

   -- I am using difference lists to get associativity "for free". This
   -- makes it possible to state the right-assoc lemma below without
   -- using any casts.

   record TypeList : Set1 where
     infixr 5 _⟶_
     field
       _⟶_    : Set -> Set
       map    : forall {a b} -> (a -> b) -> _⟶_ a -> _⟶_ b
       map-id : forall a -> map (id {A = a}) ≡ id
       map-∘  : forall {a b c} (f : b -> c) (g : a -> b) ->
                map (f ∘ g) ≡ map f ∘ map g

The other:

   -- Families of functions which, on the semantic side, correspond to
   -- the application of a given context morphism

   record [_⟶_] {t₁ t₂} (T₁ : Term-like t₁) (T₂ : Term-like t₂)
                {Γ Δ : Ctxt} (ρ̂ : Γ ⇨̂ Δ) : Set (i ⊔ u ⊔ e ⊔ t₁ ⊔ t₂) where
     constructor _,_

     open Term-like T₁ renaming (_⊢_ to _⊢₁_; ⟦_⟧ to ⟦_⟧₁)
     open Term-like T₂ renaming (_⊢_ to _⊢₂_; ⟦_⟧ to ⟦_⟧₂)

     field
       function     : ∀ σ → Γ ⊢₁ σ → Δ ⊢₂ σ /̂ ρ̂
       .corresponds :
          ∀ σ (t : Γ ⊢₁ σ) → ⟦ t ⟧₁ /̂Val ρ̂ ≅-Value ⟦ function σ t ⟧₂

In this case the identity and associativity laws hold by definition
(because they hold automatically for function composition/identity).
However, in the end I decided not to use this approach, because I didn't
want to rely on yet another not-universally-accepted feature of Agda.

--

-- 
/NAD
Alan Jeffrey | 4 Nov 19:01 2011

Re: Associativity for free!

On 11/04/2011 05:48 AM, Nils Anders Danielsson wrote:
> On 2011-10-26 16:48, Alan Jeffrey wrote:
>> 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?
>
> I've used the two tricks independently, but I haven't seen them used
> together.

This is my feeling, that the two tricks have been kicking around for a 
while, and this is just the requisite bit of glue to stick them together.

> However, in the end I decided not to use this approach, because I didn't
> want to rely on yet another not-universally-accepted feature of Agda.

Indeed. I'm on thin ice here, as the postulate for relevance of 
propositional equality is a bit dodgy. I'm not entirely sure how it 
would be formalized in homotopy types (it implies that there is a 
canonical path between any two connected points, but who knows what that 
does to the theory).

A.

Gmane