headers
KINOSHITA Yoshiki | 1 Nov 2011 13:57
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>
(Continue reading)

Permalink | Reply | 3 comments |
headers
Alan Jeffrey | 2 Nov 2011 17:26
Favicon
Gravatar

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

Permalink | Reply | 20 comments |
headers
Andreas Abel | 2 Nov 2011 18:46
Picon
Favicon

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

Permalink | Reply | 3 comments |
headers
Andreas Abel | 2 Nov 2011 18:48
Picon
Favicon

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

Permalink | Reply | 2 comments |
headers
Peter Hancock | 2 Nov 2011 21:12
Favicon

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
Permalink | Reply | 0 comments |
headers
Alan Jeffrey | 2 Nov 2011 22:10
Favicon
Gravatar

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

Permalink | Reply | 1 comment |
headers
KINOSHITA Yoshiki | 3 Nov 2011 02:25
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.
Permalink | Reply | 0 comments |
headers
Thorsten Altenkirch | 3 Nov 2011 10:39
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.
(Continue reading)

Permalink | Reply | 1 comment |
headers
Thorsten Altenkirch | 3 Nov 2011 11:50
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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Nils Anders Danielsson | 3 Nov 2011 18:19
Picon
Picon

Re: Do-notation with mix fix binders?

On 2011-10-27 11:57, Jean-Philippe Bernardy wrote:
> I think that it is known how to change the parser to drop the "do"
> part (Nils Anders& Ulf have a paper about it) but it is not currently
> implemented in Agda.

I'm not sure exactly what you are referring to here. Can you explain?

--

-- 
/NAD
Permalink | Reply | 0 comments |

Gmane