Yoneda was Re: [Agda] Associativity for free!

[Thorsten Altenkirch]

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 at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda