Haskell 的 monad 转换器在分类术语中是什么?
作为一名数学学生,当我了解 Haskell 中的 monad 时,我做的第一件事就是检查它们是否确实是我所知道的意义上的 monad。但后来我了解了 monad 转换器,而它们似乎并不完全是范畴论中研究的东西。
特别是,我希望它们与分配律相关,但它们似乎确实不同:单子变换器预计适用于任意单子,而分配律是单子和特定其他单子之间的事情。
另外,看看 monad 转换器的常见示例,当 MaybeT m
与 Maybe
组合 m
时,StateT m
是不是 m
与 State
任意顺序的组合。
所以我的问题是分类语言中的 monad 转换器是什么?
As a math student, the first thing I did when I learned about monads in Haskell was check that they really were monads in the sense I knew about. But then I learned about monad transformers and those don't quite seem to be something studied in category theory.
In particular I would expect them to be related to distributive laws but they seem to be genuinely different: a monad transformer is expected to apply to an arbitrary monad while a distributive law is an affair between a monad and a specific other monad.
Also, looking at the usual examples of monad transformers, while MaybeT m
composes m
with Maybe
, StateT m
is not a composition of m
with State
in either order.
So my question is what are monad transformer in categorical language?
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
发布评论
评论(3)
Monad 转换器在数学上并不是很令人愉快。然而,我们可以从免费单子中获得很好的(共)产品,更一般地说,理想单子:参见 Ghani 和 Uustalu 的“理想单子的副产品”:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4。 2698
Monad transformers aren't exceedingly mathematically pleasant. However, we can get nice (co)products from free monads, and, more generally, ideal monads: See Ghani and Uustalu's "Coproducts of Ideal Monads": http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.4.2698
使用范畴论计算 monad 转换器Oleksandr Manzyuk 的strong> 是另一篇关于 Monad 转换器的文章,并将该概念与重要概念联系起来范畴论中的附加。
在我看来,它还使用了范畴论最令人愉快的特征,即图表追逐,这自然化了这个概念。
希望这有帮助。
Calculating monad transformers with category theory by Oleksandr Manzyuk is another article on the Monad transformers, and relates the concept to the important concept of adjunction in the category theory.
Also it uses the most pleasant feature of the category theory, in my opinion, i.e. diagram-chasing, which naturalises the concept a lot.
Hope this helps.
单子变换器是单子类别中的尖头函子。 “问题是什么?”
这里有更多细节:
从某个类别开始,在其中我们认为那些 endofunctors M 是单子。所有这些单子 M 形成一个范畴,其态射是自然变换 M → M 。 M' 满足单子态射定律。
单子转换器是此类单子中的尖头函子。此类单子中的内函子 T 是什么?该内函子是从单子 M 到单子 T(M) 的映射,以及任何单子态射 M → T(M) 的映射。 M' 转化为单子态射 T(M) -> T(M')。
如果存在从恒等内函子 (Id) 到 T 的自然变换,则内函子 T 是“有指向的”
。恒等内函子是单子和单子态射的恒等映射。自然变换Id~> T由其在所有单子M处的分量定义。其在M处的分量是单子态射M→T。 T(M)。此外,必须有一个自然性法则(“一元自然性”),它规定,对于任何单子 M 和 M' 以及任何单子态射 M → M',由M、M'、T(M)、T(M')组成的图通勤。
该数据或多或少与 monad 转换器所需的常用数据一致。所需的单子态射 M -> T(M) 是将“外来”单子 M 提升为转换后的单子。
该构造还包括“提升”函数(这是内函子 T 对单子态射的作用),它将单子态射提升为 M -> 。 M'到T(M)-> T(M')。
如果我们考虑恒等单子 T(Id) 的图像,这一定是其他单子。称其为变压器的“基本单子”并用 B 表示。然后我们有单子态射 B ~> 。 T(M) 对于任何 M。这是从基础单子到转换后单子的提升。
然而,这个定义排除了“非函数”单子变换器,例如连续单子和代码密度单子的变换器。
分配律仅与某些单子变换器相关。存在分配律的变换器有两种:对于这些变换器,自然变换Id→M处的分量Id→→。 T由M→M给出。 B∘M 或 M ->M∘B。但其他单子具有不是函子组合的变压器,并且它们没有分配律。
更多详细信息,请参阅即将出版的《函数式编程科学》一书的第 14 章:https://github。 com/winitzki/sofp
A monad transformer is a pointed endofunctor in the category of monads. "What's the problem?"
Here are some more details:
Start with some category, in which we consider those endofunctors M that are monads. All those monads M form a category whose morphisms are natural transformations M -> M' that satisfy the laws of monad morphisms.
A monad transformer is a pointed endofunctor in this category of monads. What is an endofunctor T in this category of monads? This endofunctor is a mapping from a monad M to a monad T(M), together with a mapping of any monad morphism M -> M' into a monad morphism T(M) -> T(M').
The endofunctor T is "pointed" if there exists a natural transformation from the identity endofunctor (Id) to T.
The identity endofunctor is an identity map of monads and monad morphisms. A natural transformation Id ~> T is defined by its components at all the monads M. Its component at M is a monad morphism M -> T(M). In addition, there must be a naturality law ("monadic naturality") which says that, for any monads M and M' and any monad morphism M -> M', the diagram consisting of M, M', T(M), T(M') commutes.
This data more or less coincides with the usual data required of a monad transformer. The required monad morphism M -> T(M) is the lifting of the "foreign" monad M into the transformed monad.
The construction also includes the "hoist" function (this is the action of the endofunctor T on monad morphisms), that lifts monad morphisms M -> M' to T(M) -> T(M').
If we consider the image of the identity monad, T(Id), this must be some other monad. Call that the "base monad" of the transformer and denote it by B. We have then the monad morphism B ~> T(M) for any M. This is the lifting from the base monad to the transformed monad.
However, this definition excludes the "non-functorial" monad transformers, such as that of the continuation monad and the codensity monad.
The distributive laws are only relevant to certain monad transformers. There are two kinds of transformers where distributive laws exist: for these transformers, the component at M of the natural transformation Id ~> T is given either by M -> B∘M or by M ->M∘B. But other monads have transformers that are not functor compositions, and there are no distributive laws for them.
More details are written up in Chapter 14 of the upcoming book "The Science of Functional Programming": https://github.com/winitzki/sofp