Then encodes the continuation passed to >>= in the same way as Coyoneda encodes the function passed to fmap; you can in fact arrive at a definition of Freer using Coyoneda:
data Freer f a where
Return :: a -> Freer f a
Then :: f b -> (b -> Freer f a) -> Freer f a
is isomorphic to
data Coyoneda f a where
Coyoneda :: (b -> a) -> f b -> Coyoneda f a
data Freer f a where
Return :: a -> Freer f a
Then :: Coyoneda f (Freer f a) -> Freer f a
and indeed to
newtype Freer f a = Freer { runFreer :: Either a (Coyoneda f (Freer f a)) }
This isn’t really documented but it’s pretty significant.
Then
encodes the continuation passed to>>=
in the same way asCoyoneda
encodes the function passed tofmap
; you can in fact arrive at a definition ofFreer
usingCoyoneda
:is isomorphic to
and indeed to
This isn’t really documented but it’s pretty significant.