当前位置：文江博客话题详情

Monad 作为附加词

发布于 2024-10-12 06:42:03 字数 112 浏览 6 评论 0 原文

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

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

梦里泪两行 2024-10-19 06:42:03

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

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

我将明确而简单地处理状态 monad。此代码使用 Transformers 包中的 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

无论如何，我们现在可以从我们的单位/单位附加词中定义一个 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正是我们经典的状态单子。请注意，我们可以采用相反的组合并得到 Costa Comonad（又名商店 comonad）。

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

Derek Elkins 在 The Monad Reader 13 中的文章以不同的方式介绍了这些材料——使用类别理论计算 Monad：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

旧答案：

两个参考文献。

1) 类别附加一如既往地提供了附加词的表示以及单子如何从中产生。像往常一样，思考很好，但文档很少： http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor-Adjunction.html

2) -咖啡馆还对辅助的作用进行了有希望但简短的讨论。其中一些可能有助于解释类别附加内容： http:// www.haskell.org/pipermail/haskell-cafe/2007-December/036328.html

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

回复收藏 0 原文

忆伤 2024-10-19 06:42:03

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

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

回复收藏 0 原文

那片花海 2024-10-19 06:42:03

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

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

让 T 为列表 monad T 。 T,eta,mu >（eta = return 和 mu = concat）并考虑 T 代数 h:T a ->一个。

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

根据定义，h 必须满足 hT h == h.mu a 并且h.eta a== id。

现在，一些简单的图表追踪证明了 h 实际上在 a 上引入了幺半群结构（由 x*y = h[x,y] 定义），
并且 h 成为该结构的幺半群同态。

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

这样（h =foldr ( * ) a0，一个将 (:) 替换为 (*) 的函数，并映射 < code>[] 到 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 ，上面折叠函数定义的自然变换
（从自由幺半群到其商幺半群的“正则满射”）

接下来，还有另一个“克莱斯利范畴”和相应的附加项。
您可以检查它是否只是具有态射的 Haskell 类型的类别 a ->; Tb，其中其成分由所谓的“Kleisli 成分”(>=>) 给出。典型的 Haskell 程序员会发现这个类别更熟悉。

最后，如CWM所示，T-代数的范畴
（分别为 Kleisli 范畴）成为范畴中的终端（分别为初始）对象
以适当的方式定义列表单子 T 的形容词。

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

This is an old thread, but I found the question interesting,
so I did some calculations myself. Hopefully Bartosz is still there
and might read this..

In fact, the Eilenberg-Moore construction does give a very clear picture in this case.
(I will use CWM notation with Haskell like syntax)

Let T be the list monad < T,eta,mu > (eta = return and mu = concat)
and consider a T-algebra h:T a -> a.

(Note that T a = [a] is a free monoid <[a],[],(++)>, that is, identity [] and multiplication (++).)

By definition, h must satisfy h.T h == h.mu a and h.eta a== id.

Now, some easy diagram chasing proves that h actually induces a monoid structure on a (defined by x*y = h[x,y] ),
and that h becomes a monoid homomorphism for this structure.

Conversely, any monoid structure < a,a0,* > defined in Haskell is naturally defined as a T-algebra.

In this way (h = foldr ( * ) a0, a function that 'replaces' (:) with (*),and maps [] to a0, the identity).

So, in this case, the category of T-algebras is just the category of monoid structures definable in Haskell, HaskMon.

(Please check that the morphisms in T-algebras are actually monoid homomorphisms.)

It also characterizes lists as universal objects in HaskMon, just like free products in Grp, polynomial rings in CRng, etc.

The adjuction corresponding to the above construction is < F,G,eta,epsilon >

where

F:Hask -> HaskMon, which takes a type a to the 'free monoid generated by a',that is, [a],
G:HaskMon -> Hask, the forgetful functor (forget the multiplication),
eta:1 -> GF , the natural transformation defined by \x::a -> [x],
epsilon: FG -> 1 , the natural transformation defined by the folding function above
(the 'canonical surjection' from a free monoid to its quotient monoid)

Next, there is another 'Kleisli category' and the corresponding adjunction.
You can check that it is just the category of Haskell types with morphisms a -> T b,
where its compositions are given by the so-called 'Kleisli composition' (>=>).
A typical Haskell programmer will find this category more familiar.

Finally,as is illustrated in CWM, the category of T-algebras
(resp. Kleisli category) becomes the terminal (resp. initial) object in the category
of adjuctions that define the list monad T in a suitable sense.

I suggest to do a similar calculations for the binary tree functor T a = L a | B (T a) (T a) to check your understanding.

回复收藏 0 原文

長街聽風 2024-10-19 06:42:03

我已经找到了 Eilenberg-Moore 为任何 monad 附加函子的标准结构，但我不确定它是否增加了对问题的任何见解。构造中的第二个类别是 T 代数类别。 AT代数在初始类别中添加了“乘积”。

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

我必须说我一无所知。

回复收藏 0 原文

書生途 2024-10-19 06:42:03

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

首先，对于给定的单子 T ，存在 T 的 Kleisli 类别的唯一附加物。
在 Haskell 中，monad 的使用主要限于此类别的操作
（本质上是一类自由代数，没有商）。
事实上，人们对 Haskell Monad 所能做的就是构造一些 Kleisli 态射
通过使用 do 表达式、(>>=) 等输入 a->T b 来创建一个新的态射。在这种情况下，单子的作用仅限于经济符号。利用态射的结合性能够编写（例如）[0,1,2] 而不是 (Cons 0 (Cons 1 (Cons 2 Nil)))，即可以将序列写为序列，不像一棵树。

甚至 IO monad 的使用也不是必需的，因为当前的 Haskell 类型系统很强大
足以实现数据封装（存在类型）。

这是我对你原来问题的回答，
但我很好奇 Haskell 专家对此有何评论。

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

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

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

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

最后，一些评论：

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

If you are interested,here's some thoughts of a non-expert
on the role of monads and adjunctions in programming languages:

First of all, there exists for a given monad T a unique adjunction to the Kleisli category of T.
In Haskell,the use of monads is primarily confined to operations in this category
(which is essentially a category of free algebras,no quotients).
In fact, all one can do with a Haskell Monad is to compose some Kleisli morphisms of
type a->T b through the use of do expressions, (>>=), etc., to create a new
morphism. In this context, the role of monads is restricted to just the economy
of notation.One exploits associativity of morphisms to be able to write (say) [0,1,2]
instead of (Cons 0 (Cons 1 (Cons 2 Nil))), that is, you can write sequence as sequence,
not as a tree.

Even the use of IO monads is non essential, for the current Haskell type system is powerful
enough to realize data encapsulation (existential types).

This is my answer to your original question,
but I'm curious what Haskell experts have to say about this.

On the other hand, as we have noted, there's also a 1-1 correspondence between monads and
adjunctions to (T-)algebras. Adjoints, in MacLane's terms, are 'a way
to express equivalences of categories.'
In a typical setting of adjunctions <F,G>:X->A where F is some sort
of 'free algebra generator' and G a 'forgetful functor',the corresponding monad
will (through the use of T-algebras) describe how (and when) the algebraic structure of A is constructed on the objects of X.

In the case of Hask and the list monad T, the structure which T introduces is that
of monoid,and this can help us to establish properties (including the correctness) of code through algebraic
methods that the theory of monoids provides. For example, the function foldr (*) e::[a]->a can
readily be seen as an associative operation as long as <a,(*),e> is a monoid,
a fact which could be exploited by the compiler to optimize the computation (e.g. by parallelism).
Another application is to identify and classify 'recursion patterns' in functional programming using categorical
methods in the hope to (partially) dispose of 'the goto of functional programming', Y (the arbitrary recursion combinator).

Apparently, this kind of applications is one of the primary motivations of the creators of Category Theory (MacLane, Eilenberg, etc.),
namely, to establish natural equivalence of categories, and transfer a well-known method in one category
to another (e.g. homological methods to topological spaces,algebraic methods to programming, etc.).
Here, adjoints and monads are indispensable tools to exploit this connection of categories.
(Incidentally, the notion of monads (and its dual, comonads) is so general that one can even go so far as to define 'cohomologies' of
Haskell types.But I have not given a thought yet.)

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