单子作为附属词

编辑：只是为了好玩，我会做对的。原始答案保留在下面

category-extras 的当前附加代码现在位于附加包中：http://hackage.haskell.org/package/adjunctions

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

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

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 中的恒等函子。

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

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，如下所示：

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 ->) 之间的经典连接：

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（又名商店 comonad）。

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

Derek Elkins 在 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 之间的附加词构建列表单子：http://www.cs.ox.ac.uk/ralf.hinze/Kan.pdf

老答案：

两个参考。

1) 与往常一样，Category-extras 提供了附加词的表示以及单子如何从它们中产生。像往常一样，考虑一下很好，但文档很简单：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

---

Derek Elkins 最近在晚餐时向我展示了 Cont Monad 是如何通过与自身组合 (_ -> k) 逆变函子而产生的，因为它恰好是自伴的。这就是您摆脱(a -> k) -> k的方式。然而，它的 counit 会导致双重否定消除，这不能用 Haskell 编写。

有关说明和证明这一点的一些 Agda 代码，请参阅 http://hpaste.org/68257。

---

这是一个旧线程，但我发现这个问题很有趣，所以我自己做了一些计算。希望 Bartosz 还在那里，并且可能会读到这个..

事实上，Eilenberg-Moore 结构在这种情况下确实给出了非常清晰的图景。 （我将使用 CWM 表示法和类似 Haskell 的语法）

令 T 为列表单子 < T,eta,mu >（eta = return 和 mu = concat）并考虑 T 代数 h:T a -> a。

（注意 T a = [a] 是一个自由幺半群 <[a],[],(++)>，即恒等式 [] 和乘法 (++)。）

根据定义，h 必须满足 h.T h == h.mu a 和 h.eta a== id。

现在，一些简单的图表追逐证明 h 实际上在 a（由 x*y = h[x,y] 定义）上诱导出一个幺半群结构，并且h 成为这个结构的一个幺半群同态。

相反，在 Haskell 中定义的任何幺半群结构 < a,a0,* > 自然地定义为 T 代数。

以这种方式（h = foldr ( * ) a0，一个用 (*) '替换' (:) 并将 [] 映射到 a0 的函数，即身份）。

因此，在这种情况下，T 代数的范畴只是在 Haskell，HaskMon 中定义的幺半群结构的范畴。

（请检查 T 代数中的态射实际上是幺半群同态。）

它还将列表表征为 HaskMon 中的通用对象，就像 Grp 中的免费产品、CRng 中的多项式环等一样。

与上述结构对应的增补是< F,G,eta,epsilon >

在哪里

F:Hask -> HaskMon，将类型a取为'由a生成的自由幺半群'，即[a]，

G:HaskMon -> Hask，健忘函子（忘记乘法），

eta:1 -> GF ，由 \x::a -> [x] 定义的自然变换，

epsilon: FG -> 1 ，由上面的折叠函数定义的自然变换（从自由幺半群到其商幺半群的“规范满射”）

接下来，还有另一个“Kleisli 类别”和相应的附加词。您可以检查它是否只是具有态射 a -> T b 的 Haskell 类型的类别，其中它的组合由所谓的“Kleisli 组合”(>=>) 给出。一个典型的 Haskell 程序员会发现这个类别更熟悉。

最后，如 CWM 所示，T 代数的范畴（分别是 Kleisli 范畴）成为在适当意义上定义列表单子 T 的附加范畴中的终端（分别是初始）对象。

我建议对二叉树函子 T a = L a | B (T a) (T a) 进行类似的计算，以检查您的理解。

---

我已经为 Eilenberg-Moore 的任何 monad 找到了附加函子的标准结构，但我不确定它是否为问题增加了任何洞察力。构造中的第二类是T-代数的范畴。 AT 代数在初始类别中添加了一个“产品”。

那么它如何用于列表单子呢？ list monad 中的函子由一个类型构造函数组成，例如 Int->[Int] 和一个函数映射（例如，映射到列表的标准应用程序）。代数添加了从列表到元素的映射。一个例子是添加（或相乘）整数列表的所有元素。函子 F 采用任何类型，例如 Int，并将其映射到 Int 列表中定义的代数中，其中乘积由 monadic join 定义（反之亦然，join 定义为乘积）。健忘函子 G 接受代数并忘记乘积。伴随函子对 F, G 然后用于以通常的方式构造 monad。

我必须说我一点也不聪明。

---

如果您有兴趣，这里有一些非专家关于单子和附属词在编程语言中的作用的想法：

首先，对于给定的 monad T，存在对 Kleisli 类别 T 的唯一附加项。在 Haskell 中，monad 的使用主要局限于这一类的运算（本质上是一个自由代数的范畴，没有商）。事实上，使用 Haskell Monad 所能做的就是通过使用 do 表达式、(>>=) 等组合一些 a->T b 类型的 Kleisli 态射，以创建一个新的态射。在这种情况下，monad 的作用仅限于符号的经济性。利用态射的结合性可以写（比如）[0,1,2] 而不是 (Cons 0 (Cons 1 (Cons 2 Nil)))，也就是说，您可以将序列写为序列，而不是作为一棵树。

即使使用 IO monads 也不是必须的，因为当前的 Haskell 类型系统已经足够强大，可以实现数据封装（存在类型）。

这是我对您最初问题的回答，但我很好奇 Haskell 专家对此有何看法。

另一方面，正如我们所指出的，单子和 (T-) 代数的附属词之间也存在 1-1 对应关系。用麦克莱恩的话来说，伴随词是“一种表达类别等价性的方式”。在附词 <F,G>:X->A 的典型设置中，其中 F 是某种“自由代数生成器”，G 是“健忘函子”，相应的单子将（通过使用 T 代数）描述如何（以及何时） A 的代数结构是在 X 的对象上构造的。

在 Hask 和列表 monad T 的情况下，T 引入的结构是幺半群的结构，这可以帮助我们通过幺半群理论提供的代数方法来建立代码的属性（包括正确性）。例如，只要 <a,(*),e> 是一个幺半群，函数 foldr (*) e::[a]->a 就可以很容易地被视为一个关联操作，编译器可以利用这一事实来优化计算（例如通过并行性）。另一个应用是使用分类方法识别和分类函数式编程中的“递归模式”，希望（部分）处理“函数式编程的 goto”，Y（任意递归组合器）。

显然，这种应用是范畴论的创造者（MacLane、Eilenberg 等）的主要动机之一，即建立范畴的自然对等，并将一个范畴中的一个众所周知的方法转移到另一个范畴（例如拓扑空间的同调方法，编程的代数方法等）。在这里，伴随物和单子是利用这种类别联系的不可或缺的工具。 （顺便说一句，单子（及其对偶的共单子）的概念是如此普遍，以至于人们甚至可以定义 Haskell 类型的“上同调”。但我还没有考虑过。）

至于你提到的非确定性函数，我要说的要少得多……但请注意；如果某个类别 A 的附加 <F,G>:Hask->A 定义了列表 monad T，则必须有一个唯一的“比较函子”K:A->MonHask（可在 Haskell 中定义的幺半群类别），请参阅 CWM。这实际上意味着，您感兴趣的类别必须是某种受限形式的幺半群（例如，它可能缺少一些商，但没有自由代数）才能定义列表单子。

最后，几点说明：

我在上一篇文章中提到的二叉树函子很容易推广到任意数据类型 T a1 .. an = T1 T11 .. T1m | ...。也就是说，Haskell 中的任何数据类型都自然定义了一个 monad（连同相应的代数范畴和 Kleisli 范畴），这只是 Haskell 中的任何数据构造函数求和的结果。这是我认为 Haskell 的 Monad 类只不过是语法糖的另一个原因（当然，这在实践中非常重要）。

---