We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies.

We use cookies and other tracking technologies to improve your browsing experience on our site, analyze site traffic, and understand where our audience is coming from. To find out more, please read our privacy policy.

By choosing 'I Accept', you consent to our use of cookies and other tracking technologies. Less

We use cookies and other tracking technologies... More

Login or register
to publish this job!

Login or register
to save this job!

Login or register
to save interesting jobs!

Login or register
to get access to all your job applications!

Login or register to start contributing with an article!

Login or register
to see more jobs from this company!

Login or register
to boost this post!

Show some love to the author of this blog by giving their post some rocket fuel ๐Ÿš€.

Login or register to search for your ideal job!

Login or register to start working on this issue!

Login or register
to save articles!

Login to see the application

Engineers who find a new job through Functional Works average a 15% increase in salary ๐Ÿš€

You will be redirected back to this page right after signin

Blog hero image

Yoneda as "Enriched Continuations"

Siddharth Bhat 5 November, 2021 | 2 min read

Yoneda as enriched continuations

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 Kontinuation. 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".

Related Issues

open-editions / corpus-joyce-ulysses-tei
open-editions / corpus-joyce-ulysses-tei
  • Started
  • 0
  • 2
  • Intermediate
  • HTML
open-editions / corpus-joyce-ulysses-tei
open-editions / corpus-joyce-ulysses-tei
  • Started
  • 0
  • 2
  • Intermediate
  • HTML
open-editions / corpus-joyce-ulysses-tei
open-editions / corpus-joyce-ulysses-tei
  • Open
  • 0
  • 0
  • Intermediate
  • HTML
open-editions / corpus-joyce-ulysses-tei
open-editions / corpus-joyce-ulysses-tei
  • Started
  • 0
  • 1
  • Intermediate
  • HTML

Get hired!

Sign up now and apply for roles at companies that interest you.

Engineers who find a new job through Functional Works average a 15% increase in salary.

Start with GitHubStart with Stack OverflowStart with Email