由于 State monad 可以分解为 Product(左 - Functor)和 Reader(右 - 可表示)。
-- 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
最佳答案
这不会进行类型检查,因为类 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
类,因此我们可以对不同类别之间的附加进行建模: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)(如果我们翻转附加词,也是一个共单子(monad)):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 (=<<)
我不知道延续单子(monad)是否对应于 Hask 上的 endofunctors 之间的附属物。
另请参阅有关 monad 的 nCatLab 文章: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.
关于haskell - 如何将延续单子(monad)分解为左右伴随?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/61267827/