单子作为附件 [英] Monads as adjunctions

问题描述

我一直在阅读关于范畴论中的单子.单子的一个定义使用一对伴随函子.monad 由使用这些函子的往返定义.显然附属在范畴论中非常重要，但我还没有看到任何关于伴随函子的 Haskell monad 的解释.有人考虑过吗?

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

类别附加的当前附加代码现在在附加包中:http://hackage.haskell.org/package/adjunctions

The current adjunction code for category-extras now is in the adjunctions package: http://hackage.haskell.org/package/adjunctions

我只是要明确而简单地处理状态 monad.此代码使用来自转换器包的 Data.Functor.Compose，但在其他方面是独立的.

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.

f (D -> C) 和 g (C -> D) 之间的附加词，写作 f -|g, 可以用多种方式表征.我们将使用 counit/unit (epsilon/eta) 描述，它给出了两个自然变换(函子之间的态射).

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)

注意，counit 中的a"实际上是 C 中的恒等函子，而 unit 中的a"实际上是 D 中的恒等函子.

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.

我们还可以从 counit/unit 定义中恢复 hom-set 附加定义.

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

无论如何，我们现在可以从我们的 unit/counit 附属定义一个 Monad，如下所示:

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

现在我们可以实现 (a,) 和 (a ->) 之间的经典附加:

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)

现在是类型同义词

type State s = Compose ((->) s) ((,) s)

如果我们在 ghci 中加载它，我们可以确认 State 正是我们的经典 state monad.请注意，我们可以采用相反的组合并获得 Costate Comonad(又名 store comonad).

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

我们可以用这种方式将许多其他的附加词加入 monad 中(例如 (Bool,) Pair)，但它们是有点奇怪的 monad.不幸的是，我们不能以一种愉快的方式直接在 Haskell 中进行引出 Reader 和 Writer 的附加.我们可以做 Cont，但正如 copumpkin 所描述的，这需要来自相反类别的附加，所以它实际上使用了Adjoint"类型类的不同形式"，它反转了一些箭头.该表单也在 adjunctions 包的不同模块中实现.

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.

德里克·埃尔金斯 (Derek Elkins) 在 The Monad Reader 13 -- Calculating Monads with Category Theory 中的文章以不同的方式涵盖了此材料:http://www.haskell.org/wikiupload/8/85/TMR-Issue13.pdf

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

此外，Hinze 最近的 Kan Extensions for Program Optimization 论文从 Mon 和 Set 之间的附属物介绍了列表 monad 的构建:http://www.cs.ox.ac.uk/ralf.hinze/Kan.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

旧答案:

两个参考.

1) Category-extras 一如既往地提供附加的表示以及 monad 是如何从它们产生的.像往常一样，考虑一下很好，但文档很简单:http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

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 还提供了关于辅助作用的有希望但简短的讨论.其中一些可能有助于解释类别附加:http://www.haskell.org/pipermail/haskell-cafe/2007-December/036328.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

这篇关于单子作为附件的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！