We're planting a tree for every job application! Click here to learn more

Yoneda as "Enriched Continuations"

Siddharth Bhat

5 Nov 2021

2 min read

Yoneda as "Enriched Continuations"
  • Haskell

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

Did you like this article?

Siddharth Bhat

mathematics ⋂ computation

See other articles by Siddharth

Related jobs

See all

Title

The company

  • Remote

Title

The company

  • Remote

Title

The company

  • Remote

Title

The company

  • Remote

Related articles

JavaScript Functional Style Made Simple

JavaScript Functional Style Made Simple

Daniel Boros

12 Sep 2021

JavaScript Functional Style Made Simple

JavaScript Functional Style Made Simple

Daniel Boros

12 Sep 2021

WorksHub

CareersCompaniesSitemapFunctional WorksBlockchain WorksJavaScript WorksAI WorksGolang WorksJava WorksPython WorksRemote Works
hello@works-hub.com

Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ

108 E 16th Street, New York, NY 10003

Subscribe to our newsletter

Join over 111,000 others and get access to exclusive content, job opportunities and more!

© 2023 WorksHub

Privacy PolicyDeveloped by WorksHub