Monads作为附件 [英] Monads as adjunctions
问题描述
现在，category-extras的当前附加代码位于附件包中： http://hackage.haskell.org/package/adjunctions
我只是想通过状态monad明确而简单地。这段代码使用了变量包中的 Data.Functor.Compose ，但它是自包含的。
在f（D→C）和g（C→D）之间，写成f - | g，可以用多种方法表征。我们将使用counte / unit（epsilon / eta）描述，它给出了两个自然变换（仿函数之间的态射）。
class（Functor f，Functor g）=>伴随f g，其中
counit :: f（g a） - > a
unit :: a - > g（fa）
请注意，counter中的a实际上是C中的身份仿函数，单位中的a实际上是D中的身份仿函数。我们还可以从COUNT /单元定义中恢复同位置附属定义。
phiLeft :: Adjoint fg => （f a - > b） - > （a - > g b）
phiLeft f = fmap f。单位
phiRight ::伴随f g => （a - > g b） - > （f a - > b）
phiRight f = counit。在任何情况下，我们现在可以从我们的单位/议会类型中定义一个Monad，如下所示：fmap f
实例Adjoint fg => Monad（Compose g f）其中
return x = Compose $ unit x
x>>> = f =撰写。 fmap counit。 getCompose $ fmap（getCompose.f）x
现在我们可以实现（a，）之间的经典连接和（a - >）：
实例伴随（（，）a）（（ - >）a）其中
- counit ::（a，a - > b） - > b
counit（x，f）= f x
- unit :: b - > （a - >（a，b））
unit x = \ y - > （y，x）
现在是一个类型的同义词
type State s = Compose（（ - >）s）（（，）s）
如果我们用ghci加载它，我们可以确认状态正是我们经典的状态monad。请注意，我们可以采取相反的构图，并获得Costate Comonad（又名商店comonad）。
我们可以用这种方式将其他一些附加元素制作成monad （比如（Bool，）Pair），但它们有点奇怪。不幸的是，我们无法以愉快的方式直接在Haskell中引发Reader和Writer。我们可以做Cont，但是正如copumpkin所描述的那样，它需要来自相反类别的一个连接，所以它实际上使用了Adjoint类型类型的一个不同的形式，以反转一些箭头。这种形式也在辅助包中的一个不同的模块中实现。
这个材料被Derek Elkins在Monad Reader 13中的文章以不同的方式介绍 - 计算Monads与分类理论： http://www.haskell.org/wikiupload/ 8/85 / TMR-Issue13.pdf
另外，Hinze最近的程序优化的Kan扩展一书介绍了列表monad的结构 Mon 和设置： http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
老答案： 1）类别附加服务像往常一样提供辅助表示，以及monad如何从中产生。像往常一样，用文件思考是很好的，但很重要： http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html
<2> -Cafe还提供了一个很有前途但简短的关于副词作用的讨论。其中一些可能有助于解释类别额外信息： http：// www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html
I've been reading about monads in category theory. One definition of monads uses a pair of adjoint functors. A monad is defined by a round-trip using those functors. Apparently adjunctions are very important in category theory, but I haven't seen any explanation of Haskell monads in terms of adjoint functors. Has anyone given it a thought?
Edit: Just for fun, I'm going to do this right. Original answer preserved below
The current adjunction code for category-extras now is in the adjunctions package: http://hackage.haskell.org/package/adjunctions
I'm just going to work through the state monad explicitly and simply. This code uses Data.Functor.Compose from the transformers package, but is otherwise self-contained.
An adjunction between f (D -> C) and g (C -> D), written f -| g, can be characterized in a number of ways. We'll use the counit/unit (epsilon/eta) description, which gives two natural transformations (morphisms between functors).
class (Functor f, Functor g) => Adjoint f g where
counit :: f (g a) -> a
unit :: a -> g (f a)
Note that the "a" in counit is really the identity functor in C, and the "a" in unit is really the identity functor in D.
We can also recover the hom-set adjunction definition from the counit/unit definition.
phiLeft :: Adjoint f g => (f a -> b) -> (a -> g b)
phiLeft f = fmap f . unit
phiRight :: Adjoint f g => (a -> g b) -> (f a -> b)
phiRight f = counit . fmap f
In any case, we can now define a Monad from our unit/counit adjunction like so:
instance Adjoint f g => Monad (Compose g f) where
return x = Compose $ unit x
x >>= f = Compose . fmap counit . getCompose $ fmap (getCompose . f) x
Now we can implement the classic adjunction between (a,) and (a ->):
instance Adjoint ((,) a) ((->) a) where
-- counit :: (a,a -> b) -> b
counit (x, f) = f x
-- unit :: b -> (a -> (a,b))
unit x = \y -> (y, x)
And now a type synonym
type State s = Compose ((->) s) ((,) s)
And if we load this up in ghci, we can confirm that State is precisely our classic state monad. Note that we can take the opposite composition and get the Costate Comonad (aka the store comonad).
There are a bunch of other adjunctions we can make into monads in this fashion (such as (Bool,) Pair), but they're sort of strange monads. Unfortunately we can't do the adjunctions that induce Reader and Writer directly in Haskell in a pleasant way. We can do Cont, but as copumpkin describes, that requires an adjunction from an opposite category, so it actually uses a different "form" of the "Adjoint" typeclass that reverses some arrows. That form is also implemented in a different module in the adjunctions package.
this material is covered in a different way by Derek Elkins' article in The Monad Reader 13 -- Calculating Monads with Category Theory: http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf
Also, Hinze's recent Kan Extensions for Program Optimization paper walks through the construction of the list monad from the adjunction between Mon and Set: http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf
Old answer:
Two references.
1) Category-extras delivers, as as always, with a representation of adjunctions and how monads arise from them. As usual, it's good to think with, but pretty light on documentation: http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html
2) -Cafe also delivers with a promising but brief discussion on the role of adjunction. Some of which may help in interpreting category-extras: http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html
这篇关于Monads作为附件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
