How to Factorize Continuation Monad into Left & Right Adjoints?

Question

As State monad can be factorized into Product (Left - Functor) and Reader (Right - Representable).

1. Is there a way to factorize Continuation Monad? Below code is my attempt, which wont type check

-- To form a -> (a -> k) -> k
{-# LANGUAGE MultiParamTypeClasses, TypeOperators, InstanceSigs, TypeSynonymInstances #-}
type (<-:) o i = i -> o
-- I Dont think we can have Functor & Representable for this type synonym

class Isomorphism a b where
   from :: a -> b
   to :: b -> a

instance Adjunction ((<-:) e) ((<-:) e) where
   unit :: a -> (a -> e) -> e
   unit a handler = handler a

   counit :: (a -> e) -> e -> a
   counit f e = undefined -- If we have a constraint on Isomorphism a e then we can implement this

2. Is there a list of Left & Rights Adjoints that form monads?

3. I have read that, given a pair of adjoints, they form a unique Monad & Comonad but, given a Monad, it can be Factorized into multiple Factors. Is there any example of this?

Answer 1

This doesn't typecheck because the class Adjunction only represents a small subset of adjunctions, where both functors are endofunctors on Hask.

As it turns out, this is not the case for the adjunction (<-:) r -| (<-:) r. There are two subtly different functors here:

• f = (<-:) r, the functor from Hask to Op(Hask) (the opposite category of Hask, sometimes also denoted Hask^op)
• g = (<-:) r, the functor from Op(Hask) to Hask

In particular, the counit should be a natural transformation in the Op(Hask) category, which flips arrows around:

unit   :: a -> g (f a)
counit :: f (g a) <-: a

In fact, counit coincides with unit in this adjunction.

To capture this properly, we need to generalize the Functor and Adjunction classes so we can model adjunctions between different categories:

class Exofunctor c d f where
  exomap :: c a b -> d (f a) (f b)

class
  (Exofunctor d c f, Exofunctor c d g) =>
  Adjunction
    (c :: k -> k -> Type)
    (d :: h -> h -> Type)
    (f :: h -> k)
    (g :: k -> h) where
  unit :: d a (g (f a))
  counit :: c (f (g a)) a

Then we get again that Compose is a monad (and a comonad if we flip the adjunction):

newtype Compose f g a = Compose { unCompose :: f (g a) }

adjReturn :: forall c f g a. Adjunction c (->) f g => a -> Compose g f a
adjReturn = Compose . unit @_ @_ @c @(->)

adjJoin :: forall c f g a. Adjunction c (->) f g => Compose g f (Compose g f a) -> Compose g f a
adjJoin = Compose . exomap (counit @_ @_ @c @(->)) . (exomap . exomap @(->) @c) unCompose . unCompose

and Cont is merely a special case of that:

type Cont r = Compose ((<-:) r) ((<-:) r)

See also this gist for more details: https://gist.github.com/Lysxia/beb6f9df9777bbf56fe5b42de04e6c64

---

I have read that given a pair of adjoints they form a unique Monad & Comonad but given a Monad it can be Factorized into multiple Factors. Is there any example of this?

The factorization is generally not unique. Once you've generalized adjunctions as above, then you can at least factor any monad M as an adjunction between its Kleisli category and its base category (in this case, Hask).

Every monad M defines an adjunction
  F -| G
where

F : (->) -> Kleisli M
  : Type -> Type                -- Types are the objects of both categories (->) and Kleisli m.
                                -- The left adjoint F maps each object to itself.
  : (a -> b) -> (a -> M b)      -- The morphism mapping uses return.

G : Kleisli M -> (->)
  : Type -> Type                -- The right adjoint G maps each object a to m a
  : (a -> M b) -> (M a -> M b)  -- This is (=<<)

I don't know whether the continuation monad corresponds to an adjunction between endofunctors on Hask.

See also the nCatLab article on monads: https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity

Relation to adjunctions and monadicity

Every adjunction (L ⊣ R) induces a monad R∘L and a comonad L∘R. There is in general more than one adjunction which gives rise to a given monad this way, in fact there is a category of adjunctions for a given monad. The initial object in that category is the adjunction over the Kleisli category of the monad and the terminal object is that over the Eilenberg-Moore category of algebras. (e.g. Borceux, vol. 2, prop. 4.2.2) The latter is called the monadic adjunction.