18

由于 State monad 可以分解为 Product（左 - Functor）和 Reader（右 - 可表示）。

  1. 有没有办法分解Continuation 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，它可以分解为多个因子。有这方面的例子吗？

4

1 回答 1

18

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

事实证明， adjunction 并非如此(<-:) 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，它可以分解为多个因子。有这方面的例子吗？

因式分解通常不是唯一的。一旦您如上所述概括了附加词，那么您至少可以将任何 monadM作为其 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 (=<<)

我不知道延续单子是否对应于 Hask 上的 endofunctors 之间的附属物。

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

与附加词和一元性的关系

每个附加词 (L ⊣ R) 都会引出一个单子 R∘L 和一个共单子 L∘R。通常有不止一个附加词以这种方式产生一个给定的单子，实际上对于一个给定的单子有一类附加词。该范畴的初始对象是单子的 Kleisli 范畴的附属物，而终端对象是代数的 Eilenberg-Moore 范畴的附属物。(例如 Borceux, vol. 2, prop. 4.2.2) 后者被称为一元附加语。

于 2020-04-17T13:31:38.780 回答