Free monads and the Yoneda lemma

[runarorama]

This is an issue reserved for comments on the post of the same title on blog.higher-order.com

[xuwei-k]

case class Req[F[_],I,A](req: F[I], k: I => IO[F,A])

should be

case class Req[F[_],I,A](req: F[I], k: I => IO[F,A]) extends IO[F,A] 

?

[runarorama]

Yes, that's right, Kenji. Thanks!

[Blaisorblade]

I'm looking into the Yoneda lemma on Wikipedia. And trying to reconcile that with your post confuses me.

But it also requires that F[_] is a functor as hypothesis — that is, you have a function fmap: [A, B](A => B) => F[A] => F[B]. As a consequence, you of course have functions [B](A => B) => F[B]. So I find it confusing that you conclude "This also means that F is definitely a functor." - shouldn't that be the hypothesis?

Moreover, you say:

The Yoneda lemma says that this goes the other way around as well. If you have a value of type F[A] for any functor F and any type A, then you certainly have a map function with the signature above.

But attributing that to the Yoneda lemma seems wrong: F is a functor, which means directly that fmap exists and that you can apply it to a value of type F[A].

Apparently, the non-obvious thing the theorem says is that this correspondence is a isomorphism between F[A] and [B](A => B) => F[B] (so you can run the correspondence back and forth and come back to the same point, that is, that all such functions are instances of fmap), and that it is natural in F and A (that is, I'm guessing, it is parametric in those parameters). That's what you have at the end, and that's part of the Yoneda statement — but I'm confused about the rest.

[runarorama]

On the first point: what I mean is that the construction is unique. If you have [B](A => B) => F[B], then such a thing could only have been constructed by partially applying map for the functor F.

On the second point: what I mean is that the Yoneda lemma has a dual. It can be stated either as:

∀ F A. Functor[F] => (F[A] <=> ∀B. (A => B) => F[B])

Or dually:

∀ F A. Functor[F] => (F[A] <=> ∃B. (B => A, F[B]))

This latter one is interesting because F[A] => ∃B. (B => A, F[B]) even if F is not a functor.

[eulerfx]

Typo in declaration of Free?

case class Suspend[F[_],A](s: F[Free[F[A]]]) extends Free[F,A]

should be

case class Suspend[F[_],A](s: F[Free[F, A]]) extends Free[F,A]

[Blaisorblade]

@eulerfx : I agree with you.

[Blaisorblade]

@runarorama: thanks for your answers. EDIT: I've finally understood them, and realized the reasons for the differences between the standard Yoneda lemma and what you get.

I've looked at it again after getting the Yoneda lemma, and realized that it becomes much stronger in a Haskell-like programming language, because both type constructors and polymorphic functions are not arbitrary functions but obey strong restrictions. For instance, [A]F[A] => G[A] is a natural transformation thanks to parametricity, and given a type constructor F[X] we can derive a Functor instance as long as it does not use X in a contravariant position (and otherwise, we can construct from it a contravariant functor or a "mixed-variance" bifunctor — say, F[A] = A => A becomes F'[-A0, +A1] = A0 => A1).

I think that's why from [B](A => B) => F[B] you can deduce that F is a functor.

*(Now, Scala does not really have parametricity, so lots of stuff holds modulo side conditions such as "don't use null", "avoid non-termination/side effects", etc.).

[adamw]

Sorry for reviving such an old post, but I have trouble seeing how:

import scalaz._

def toYo[F[_]:Functor,A](fa: F[A]) = new Yoneda[F,A] {
  def map[B](f: A => B) = Functor[F].map(fa)(f)
}

def froYo[F[_],A](yo: Yoneda[F,A]) = yo.map(a => a)

is a proof of the Yoneda lemma. I can see how F[A] embeds into Yoneda[F, A] (different F[A]s yield different yonedas), but not other way round - different Yoneda instances don't have to behave differently on the identity function? Or maybe there's another way to see the isomorphism?

[runarorama]

@adamw The Yoneda lemma says that Yoneda[F,?] is isomorphic to F. The pair of functions toYo and froYo are only part of the proof. What remains is to show that they are inverses of each other.

fa = froYo(toYo(fa))
fa = froYo(new Yoneda[F,A] { def map[B](f: A => B) = Functor[F].map(fa)(f) })
fa = new Yoneda[F,A] { def map[B](f: A => B) = Functor[F].map(fa)(f) }.map(a => a)
fa = Functor[F].map(fa)(a => a)
fa = fa
QED.

yo = toYo(froYo(yo))
yo = toYo(yo.map(a => a))
yo = new Yoneda[F,A] {
  def map[B](f: A => B) = Functor[F].map(yo.map(a => a))(f)
}
yo = new Yoneda[F,A] {
  def map[B](f: A => B) = yo.map(f)
}
yo = yo
QED.

The latter appeals to yo.map(f) = yo.map(identity).map(f), which follows from the naturality of Yoneda[F,?] (it is a natural transformation (A => ?) ~> F). That naturality condition is expressed as a homomorphism law on the two functors (so ultimately this appeals to the functor law).

(yo map _) andThen (_ map f) = (_ compose f) andThen (yo map _)

or simply:

yo.map(g).map(f) = yo.map(g compose f)

So therefore...

yo.map(identity[A]).map(f) = yo.map(identity[A] compose f)
yo.map(identity[A]).map(f) = yo map f

[adamw]

@runarorama Thanks! The naturality argument is the part I was missing :)

[TomasMikula]

I'm still puzzled how the data type CoYoneda relates to the Yoneda lemma. There doesn't seem to be a one-to-one correspondence between the inhabitants of F[A] and the inhabitants of ∃B. (B => A, F[B])—there are many more inhabitants of the latter. I only see that they are either both inhabited or both uninhabited, but not in one-to-one correspondence.