如何将连续单声道分解为左右伴随？

Question

因为State monad可分解为乘积（左-函子）和阅读器（右-可表示）。

1. 是否有一种方法可以将延续单子分解？下面的代码是我的尝试，它不会键入检查

-- 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. 是否有构成单子的左和右伴随项列表

3. 我读过，给定一对伴随物，它们会形成一个独特的Monad＆Comonad，但给定一个Monad，它可以分解为多个因数。有这个例子吗？

Answer 1

这不会进行类型检查，因为Adjunction仅表示附加功能的一小部分，其中两个函子都是Hask上的endofunctors。

事实证明，附件(<-:) 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类进行泛化，以便可以对不同类别之间的附加语进行建模：

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是一个单子（如果您翻转该附加词则是一个同名字母）：

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

---

我已经读过，给定一对伴随物，它们形成一个独特的Monad＆Comonad，但给定一个Monad，它可以分解为多个因数。有这个例子吗？

分解通常不是唯一的。如上所述，对附加词进行了广义化之后，至少可以将任何monad M作为其Kleisli类别与其基本类别（在本例中为Hask）之间的附属词。

Every monad M is 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 (=<<)
我不知道延续单子是否对应于Hask上endofunctors之间的附加词。