82

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

4

5 回答 5

41

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

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

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

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 论文从Monand之间的附加词开始构建列表 monad 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

于 2011-01-15T22:31:48.763 回答
10

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

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

于 2011-01-15T03:05:52.077 回答
9

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

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

让我们T成为列表 monad < T,eta,mu >( eta = returnand mu = concat) 并考虑一个 T-algebra 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成为该结构的一个幺半群同态。

相反，< a,a0,* >Haskell 中定义的任何幺半群结构自然地定义为 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 类别”和相应的附加词。您可以检查它是否只是带有态射的 Haskell 类型的类别a -> T b，其中它的成分由所谓的 'Kleisli composition' 给出(>=>)。一个典型的 Haskell 程序员会发现这个类别更熟悉。

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

我建议对二叉树函子做一个类似的计算T a = L a | B (T a) (T a)来检查你的理解。

于 2011-02-26T05:04:22.480 回答
2

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

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

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

于 2011-01-15T21:51:18.390 回答
1

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

首先，对于一个给定的 monad，存在一个T对 Kleisli 范畴的唯一附加项T。在 Haskell 中，monad 的使用主要局限于这一类的运算（本质上是一个自由代数的范畴，没有商）。事实上，使用 Haskell Monad 所能做的就是a->T b通过使用 do 表达式(>>=)等组成一些类型的 Kleisli 态射，以创建一个新的态射。在这种情况下，单子的作用仅限于符号的经济性。利用态射的结合性可以写（比方说）[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引入的结构是幺半群的结构，这可以帮助我们通过幺半群理论提供的代数方法来建立代码的属性（包括正确性）。例如，该函数foldr (*) e::[a]->a可以很容易地被视为一个关联操作，只要它<a,(*),e>是一个幺半群，编译器可以利用这一事实来优化计算（例如通过并行性）。另一个应用是使用分类方法识别和分类函数式编程中的“递归模式”，希望（部分）处理“函数式编程的 goto”，Y（任意递归组合器）。

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

As for non-determistic functions you mentioned, I have much less to say... But note that; if an adjunction <F,G>:Hask->A for some category A defines the list monad T, there must be a unique 'comparison functor' K:A->MonHask (the category of monoids definable in Haskell), see CWM. This means, in effect, that your category of interest must be a category of monoids in some restricted form (e.g. it may lack some quotients but not free algebras) in order to define the list monad.

Finally,some remarks:

The binary tree functor I mentioned in my last posting easily generalizes to arbitrary data type T a1 .. an = T1 T11 .. T1m | .... Namely,any data type in Haskell naturally defines a monad (together with the corresponding category of algebras and the Kleisli category), which is just the result of any data constructor in Haskell being total. This is another reason why I consider Haskell's Monad class is not much more than a syntax sugar (which is pretty important in practice,of course).

于 2011-03-05T06:38:52.587 回答