Siddharth Bhat
5 Nov 2021
•
2 min read
In this article, we explore the Yoneda Lemma as telling us about "enriched continuations"
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE Rank2Types #-}
We begin by considering the idea of continuations:
data Cont a = Cont { useCont :: forall r. (a -> r) -> r }
Recall that the idea of a continuation is that
we create a Promise of a value a
. This value
can be extracted from a Cont a
by providing a continuation
handler of type auser : a -> r
for any return type r
.
An example usage is below:
mkCont :: a -> Cont a
mkCont a = Cont $ \auser -> a user a
k3 :: Cont Int; k3 = mkCont 3
intUser :: Int -> String
user :: String;
user = useCont k3 $ \i ->
case i of
0 -> "zero"
1 -> "one"
2 -> "two"
3 -> "three" -- this is printed
4 -> "four"
_ -> "unk"
-- | prints 3, since `user` uses the continuation `k3`
-- | to produce the number `3`.
main :: IO (); main = print user
Continuations are generally named with a k
for K
ontinuation. In the above
example, the continuation mkCont 3
is named as k3
for a continuation holding
a value of 3
. We build this continuation using mkCont 3
. This continuation
is used by the value user
, which uses the continuation k3 :: Cont Int
by
calling useCont
. We then provide a handler \i -> ...
which tells useCont
how
we wish to handle the value i
. We case-analyze on i
, and print the appropriate
English version of the value i
. The program will print out 3
, since we extracted
the value from k3 = mkCont 3
, a continuation that held the value 3
.
Is there some way we can recover the value the value 3
that was used to build the
continuation k3 = mkCont 3
? There is! If we say:
extract :: Int
extract = useCont k3 (\i -> i)
we are saying that we want to use the i
We will now consider a generalization of the above, given by the mysterious type
data ContF f a = ContF { useContF :: forall r. (a -> r) -> f r }
where when we provide a user of a
of type (a -> r)
, the continuation
produces a value of type f r
. What value does this provide? Well, first off,
if we set f = Id
, we recover the original continuations:
-- F = id .
-- idyo :: (forall x. (a -> x) -> f x) -> a
-- idyo :: (forall x. (a -> x) -> id x) -> a
idyo :: (forall x. (a -> x) -> x) -> a
idyo k = k id
-- idyo' :: a -> (forall x. (a -> x) -> f x)
-- idyo' :: a -> (forall x. (a -> x) -> id x)
idyo' :: a -> (forall x. (a -> x) -> x)
idyo' a = \k -> k a
Can we do more? Let's try picking f = []
and see what happens: the type
looks like:
ContF [] a ~ forall r. (a -> r) -> [r]
So, given a thing that uses an a
, a (a -> r)
, we produce a list of rs, [r]
.
Since we're in a pure functional language, intuitively, the only way such a thing is possible
is if we call the function (a -> r)
.
We ca show that the two sides are equal:
lemma_toyoneda :: Functor g => g x -> Yoneda g x
lemma_toyoneda g_x yoneda = fmap yoneda g_x
lemma_fromyoneda :: Functor g => Yoneda g x -> g x
lemma_fromyoneda yoneda = yoneda id
In general, the Yoneda g x
will correspond to a "functorial continuation", where given a handler (a -> r)
,
we are expected to return a f r
. The two lemmas lemma_toyoneda
and lemma_fromyoneda
assert that the
two interpretation (forall r. (a -> r) -> f r
) and (f a
) are equal! So really, all Yoneda is doing
[from one point of view] is to tell us that we can create "enriched continuations".
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!