在Adjoint functors determine monad transformers, but where's lift?中,Simon C向我们展示了...
newtype Three u f m a = Three { getThree :: u (m (f a)) }
......正如那里的答案所讨论的那样,可以给它一个instance Adjunction f u => MonadTrans (Three u f)
(* adjections * 提供它作为AdjointT
)。因此,任何Hask/Hask附加都导致单子变换器;特别地,StateT s
以这种方式从(,) s
和(->) s
之间的currying adjunction中产生。
我的跟进质询是:这种构造是否可推广到其他单子变换器?有没有一种方法可以从合适的附件中派生出其他变压器?
meta备注:我的答案最初是为西蒙·C的问题而写的。我选择把它分拆成一个自我回答的问题,因为,在重读那个问题时,我注意到我所谓的答案更多地与评论中的讨论有关,而不是与问题本身有关。另外两个密切相关的问题是Is there a monad that doesn't have a corresponding monad transformer (except IO)?和Is the composition of an arbitrary monad with a traversable always a monad?,本Q&A可以说也是对这两个问题的跟进
1条答案
按热度按时间lnlaulya1#
Simon C's construction ...
.依赖于
f
和u
是伴随的Hask endofunctors。虽然这在StateT
的情况下是可行的,但如果我们要使其更一般化,我们必须处理两个相关的问题:m
。我们可以尝试一些有趣的附加功能。特别是,每个单子都有两个附加词:Kleisli附加词和Eilenberg-Moore附加词(关于它们的分类介绍,见艾米丽Riehl,Category Theory In Context,5.2节)。在这个答案的前半部分,我将重点讨论Kleisli附加词,因为它在伪Haskell中更方便。
(By伪Haskell,我的意思是在接下来的内容中会有猖獗的符号滥用。为了让眼睛更容易,我将使用一些特殊的约定:
|->
表示不一定是类型的事物之间的Map;类似地,:
表示类似于类型签名的内容;~>
表示非Hask态射;花括号和尖括号突出显示选定的非Hask类别中的对象;.
也表示函子复合;F -| U
表示F
和U
是伴随函子。Kleisli adjunction
如果
g
是一个HaskMonad
,则在FK g
之间有一个对应的Kleisli AdjunctionFK g -| UK g
,这将我们带到g
的Kleisli范畴.........和
UK g
,这让我们回到Hask:沿着Simon C的
Three
的思路,让我们使用g
作为特征monad,变压器将在其上构建。转换器将以某种方式合并另一个Hask monad的效果,m
,我有时将其称为“基础monad”,遵循习惯的Haskell术语。如果我们试图在
FK g
和UK g
之间挤压m
,我们会遇到上面提到的第二个问题:我们需要Kleisli-g
内函子,而不是Hask内函子。除了编造,别无他法。我的意思是,我们可以为函子定义一个函子(更具体地说,是两类内函子之间的函子),这将有望将m
变成我们可以使用的东西。我将这个“更高”的函子称为HK g
。将其应用于m
应该会给予如下结果:克莱斯利上的克莱斯利
UK g . HK g m . FK g
将是一个Hask内函子,与Three
结构对应。我们进一步希望它是Hask上的单子。我们可以通过将HK g m
设置为Kleisli-g
类别上的monad来确保这一点。这意味着我们需要在Kleisli-g
上找出fmap
,return
和join
的对应项:对于
kreturn
和kjoin
,让我们尝试最简单的方法:kmap
有点复杂。fmap @m
将给予m (g a)
而不是g (m a)
,因此我们需要一种方法将g
层拉到外面。有一种方便的方法可以做到这一点,但它要求g
是aDistributive
functor:定律和分布性条件
当然,这些猜测毫无意义,除非我们能证明它们是合法的:
计算表明,composing monads with a distributive law的四个条件足以确保定律成立:
在我们的例子中,条件#1给出
kmap
恒等式、kjoin
右恒等式和kjoin
结合性;#2给出了kreturn
自然性;#3,函子复合;#4,kjoin
自然性(kjoin
左恒等式不依赖于四个条件中的任何一个)。最后的健全性检查是确定条件本身保持所需的条件。在distribute
的特定情况下,它非常强的自然属性意味着这四个条件必然适用于任何合法的Distributive
,所以我们可以开始了。Package 起来
整个
UK g . HK g m . FK g
单子可以通过将HK g m
拆分为Kleisli adjunction来导出,这与我们开始时的Kleisli adjunction完全类似,只是我们从Klesili
-g开始而不是Hask:现在我们手头有两个附加,我们可以组合它们,导致变压器附加,最后,变压器的
return
和join
:(For关于单位和计数单位的构成的范畴解释,见艾米丽Riehl,Category Theory In Context,命题4.4.4。
至于
lift
,kmap (return @g)
听起来像是一个合理的定义。这相当于distribute . fmap return
(与来自Benjamin Hodgson's answer to Simon C's question的lift
相比),根据条件#1,它简单地变为:MonadLift
定律,即tklift
必须是一个单子态射,确实成立,join
定律依赖于分配性条件#1:总结
Kleisli附加函数允许我们从任何
Distributive
单子构造一个变换子,方法是在任何其他单子的外部组合它。把所有这些放在一起,我们有:Distributive
的典型例子是函子。在另一个monad的外部组合它会得到ReaderT
:ThreeK
示例与规范的ReaderT
示例完全一致。翻转变压器和Eilenberg-Moore附加
在上面的推导中,我们将基础单子Klesli附接堆叠在特征单子附接之上。我们也可以反过来做,从基础单子的附加开始。在定义
kmap
时会发生关键的变化。由于基本单子原则上可以是任何单子,我们不想给它加上一个Distributive
约束,这样它就可以被向外拉,就像我们在上面的推导中对g
所做的那样。更适合我们的游戏计划的是,双重地,需要来自功能monad的Traversable
,以便可以将其与sequenceA
一起推入内部。这将导致一个变压器组成的feture单子的内部,而不是在外面。下面是整体特征的内部结构。我称之为
ThreeEM
,因为它也可以通过使用Eilenberg-Moore附加(而不是Kleisli)并将它们与顶部的基础单子堆叠在一起来获得,就像Simon C的Three
一样。这一事实可能与艾伦伯格-摩尔附加语和克莱西里附加语之间的二元性有关。以这种方式出现的常见变压器包括
MaybeT
和ExceptT
。这种结构有一个潜在的缺陷。
sequenceA
必须遵循分布性条件,以便示例是合法的。然而,它的Applicative
约束使得它的自然属性比distribute
的自然属性弱得多,因此这些条件并不都是免费的:Traversable
的恒等式和自然律的结果。sequenceA
保留可遍历函子上的自然变换,只要这些变换保留toList
。虽然return
是这样的,但当被视为Identity
的自然转换时,在许多常见情况下,它不是给定的。以这种方式出现的一个反例是Proxy
/Const ()
。join @m
作为Compose m m
的自然变换,保留了(<*>)
,则它将成立,但情况可能并非如此。如果sequenceA
实际上对效果进行了排序(也就是说,如果可遍历对象可以包含多个值),则join
和(<*>)
在基本单子中执行的顺序所产生的任何差异都将导致违反条件。顺便说一句,这是臭名昭著的“ListT做错了”问题的一部分:根据这种构造构建的变压器中的ListT
仅在与交换基单子一起使用时才是合法的。join @t
(作为Compose t t
的自然转换)保留toList
时成立(即,如果它不删除,复制或重新排列元素)。一个结果是,这种构造对于join
“取嵌套结构的对角线”的特征单子不起作用(通常情况下,单子也是Distributive
示例),即使我们试图通过将自己限制在可交换的基单子上来掩盖条件#3。这些限制意味着这种结构并不像人们希望的那样广泛适用。最后,
Traversable
的限制太宽泛了。我们真正需要的可能是将特征monad作为仿射可遍历对象(即,最多容纳一个元素的容器--参见this post by Oleg Grenrus了解一些镜头风格的讨论);据我所知,没有规范的Haskell类。其他可能性
到目前为止所描述的构造要求特征单子分别为
Distributive
或Traversable
。然而,总体策略并不是克莱斯利和艾伦伯格-摩尔附加语所特有的,所以可以想象在使用其他附加语的同时尝试它。通过Simon C的Three
/AdjointT
,currying adjunction导致StateT
,即使State
既不是Distributive
也不是Traversable
,这一事实可能表明这种尝试可能是富有成效的。不过,我对此并不乐观。本杰明·霍奇森(Benjamin Hodgson)在其他地方的相关讨论中推测,所有诱导单子的附加词都导致同一个变换。这听起来很有道理,因为所有这样的附加都通过唯一的函子与克莱斯利附加和艾伦伯格-摩尔附加相关联(关于这一点,见《语境中的范畴论》,命题5.2.12)。举个例子:如果我们用
ThreeK
结构尝试List
,但使用对monoid范畴的自由/遗忘附加而不是Kleisli-[]
,我们最终得到ThreeEM
/feature-on-the-inside结构将给予我们的m []
变换器,直到“ListT做错了问题”,需要join
是一个应用同态。那么,
State
和它产生变压器的第三个附加函数呢?虽然我还没有详细地计算出来,但我怀疑把distribute
和sequenceA
(在这里的结构中使用的)分别认为属于右伴随和左伴随,而不是整个特征单子更合适。在distribute
的情况下,这相当于超越了Haskell类型签名。...查看Kleisli-
g
-to-Hask函子之间的自然转换:如果我是对的,那么就有可能扭转这个答案,并根据特征单子的Kleisli附加来重新解释
Three
/AdjointT
结构。如果是这样的话,State
并没有告诉我们很多关于其他既不是Distributive
也不是Traversable
的特征monad的信息。ListT做对了
同样值得注意的是,并非所有的转换都是通过这里所看到的附加成分的合成来混合一元效果的。在 transformers 中,
ContT
和[SelectT
不遵循模式;然而,我想说它们太古怪了,不能在这个上下文中讨论(“不是monads类别上的函子”,正如文档所指出的那样)。一个更好的例子是各种“ListT done right”实现,它通过以一种不需要在转换器的绑定中对它们进行排序的方式对基本单子效应进行网格化,避免了与sequenceA
相关的非法问题(以及流丢失问题)。出于说明的目的,这里是实现的草图:在这个
ListT
中,基本单子效应既不在列表的内部也不在列表的外部。相反,它们被固定在列表的 Backbone.js 上,通过根据ListF
定义类型来使它们变得有形。以类似方式构建的相关转换器包括free-monad转换器
FreeT
,以及来自有效流库的核心monad转换器(我上面包含的“ListT done right”链接指向 pipes 文档并非巧合)。这种转换器是否与这里描述的附加堆叠策略有某种联系?我还没有仔细考虑过这件事,所以没有说出来。这似乎是个值得深思的问题。