如何将连续Monad分解为左、右附加项？

Question

作为State，可以分解为Product (左函子)和Reader (右可表示)。

1. 有一种分解连续Monad的方法吗？下面的代码是我的尝试，它不会键入

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

1. 有没有一张左、右附件的单子列表？
2. 我读过，给定一对附件，它们形成一个独特的Monad & Comonad，但是，如果是Monad，它可以被分解成多个因素。有这样的例子吗？

Answer 1

这并不是类型化，因为类Adjunction只代表一小部分附加项，其中两个函子都是Hask上的临时函子。

事实证明，附件(<-:) r -| (<-:) r的情况并非如此。这里有两个微妙不同的函子：

• f = (<-:) r，函子从Hask到Op( Hask ) (Hask的相反范畴，有时也表示从Hask^op)
• g = (<-:) r，(Hask)到Hask

的函子)

特别是，counit应该是操作(哈斯克)类别中的一种自然转换，它可以左右翻转箭头：

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是一个单块(如果我们翻转附加项，则是一个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

，我读过，给定一对附加点，它们形成一个独特的Monad & Comonad，但是给定一个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 (=<<)

我不知道连续单元是否对应于哈斯克上的内切函数之间的附加关系。

还请参阅nCatLab关于monad的文章：https://ncatlab.org/nlab/show/monad#RelationToAdjunctionsAndMonadicity

关于附加性和单一性的

关系

每一个附加点(L⊣R)都会诱导出一个单R∘L和一个comonad L∘R，通常有一个以上的附加点，从而产生一个给定的单元，实际上，对于给定的单子有一类附加关系。该范畴中的初始对象是monad的Kleisli范畴上的附加物，终端对象是代数的Eilenberg-Moore范畴上的附加物。(例如Borceux，第2卷，道具)4.2.2)后者被称为一元连接。。