如何将连续单子因式分解为左右伴随？

Question

As State monad 可以分解为 Product（左 - Functor）和 Reader（右 - Representable）。

有没有办法分解 Continuation Monad？下面的代码是我的尝试，不会输入 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

是否有形成单子的左伴随和右伴随列表？
我读过，给定一对伴随物，它们形成一个唯一的 Monad 和 Comonad，但是，给定一个 Monad，它可以分解为多个因子。有这方面的例子吗？

Answer 1

这不会进行类型检查，因为 class Adjunction 只代表一小部分附加，其中两个函子都是 Hask 上的内函子 .

事实证明，附加语 (<-:) r -| (<-:) r 并非如此。这里有两个略有不同的仿函数：

f = (<-:) r，从Hask到Op(Hask)的函子（Hask的反类，有时也记作Hask^op）
g = (<-:) r,从Op(Hask)到Hask的函子

特别是，counit 应该是 Op(Hask) 类别中的自然转换，它翻转箭头：

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

事实上，counit与这个附加语中的unit重合。

为了正确捕捉这一点，我们需要概括 Functor 和 Adjunction classes 以便我们可以对不同类别之间的附加进行建模：

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

然后我们再次得到 Compose 是一个 monad（如果我们翻转附件，则是一个 comonad）：

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

和Cont只是一个特例：

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

另请参阅此要点以获取更多详细信息：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?

因式分解通常不是唯一的。一旦你像上面那样概括了附加条件，那么你至少可以将任何 monad M 作为其 Kleisli 范畴和它的基本范畴（在本例中为 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 (=<<)

不知道continuation monad是否对应Hask上endofunctors之间的adjunction

另请参阅 nCatLab 关于 monad 的文章：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.

如何将连续单子因式分解为左右伴随？

How to Factorize Continuation Monad into Left & Right Adjoints?

monads

continuations

haskell

category-theory

comonad

Relation to adjunctions and monadicity