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 registerto boost this post!

Show some love to the author of this blog by giving their post some rocket fuel ๐.

# Login to see the application

Engineers who find a new job through Functional Works average a 15% increase in salary ๐

# Yoneda as "Enriched Continuations"

Siddharth Bhat 5 November, 2021 | 2 min read

## Yoneda as 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".

Siddharth Bhat
mathematics โ computation

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