haskell 一般来说,单子变换器是由附加词产生的吗?

xqk2d5yq  于 2023-06-30  发布在  其他
关注(0)|答案(1)|浏览(171)

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可以说也是对这两个问题的跟进

lnlaulya

lnlaulya1#

  • 这个答案中的三种结构也可以在this Gist中以可复制的形式获得。*

Simon C's construction ...

newtype Three u f m a = Three { getThree :: u (m (f a)) }

.依赖于fu是伴随的Hask endofunctors。虽然这在StateT的情况下是可行的,但如果我们要使其更一般化,我们必须处理两个相关的问题:

  • 首先,我们需要为构建转换器的“特征单子”找到合适的附加物;和
  • 其次,如果这样一个附加项使我们远离了Hask,我们将不得不以某种方式解决这样一个事实,即不可能直接使用Hask monad m

我们可以尝试一些有趣的附加功能。特别是,每个单子都有两个附加词:Kleisli附加词和Eilenberg-Moore附加词(关于它们的分类介绍,见艾米丽Riehl,Category Theory In Context,5.2节)。在这个答案的前半部分,我将重点讨论Kleisli附加词,因为它在伪Haskell中更方便。
(By伪Haskell,我的意思是在接下来的内容中会有猖獗的符号滥用。为了让眼睛更容易,我将使用一些特殊的约定:|->表示不一定是类型的事物之间的Map;类似地,:表示类似于类型签名的内容; ~>表示非Hask态射;花括号和尖括号突出显示选定的非Hask类别中的对象; .也表示函子复合; F -| U表示FU是伴随函子。

Kleisli adjunction

如果g是一个Hask Monad,则在FK g之间有一个对应的Kleisli Adjunction FK g -| UK g,这将我们带到g的Kleisli范畴......

-- Object and morphism mappings.
FK g : a          |-> {a}
       f : a -> b |-> return . f : {a} ~> {b} ~ a -> g b
-- Identity and composition in Kleisli t are return and (<=<)

...和UK g,这让我们回到Hask:

UK g : {a}            |-> g a
       f : {a} -> {b} |-> join . fmap f : g a -> g b  -- that is, (>>= f)

-- The adjunction isomorphism:
kla : (FK g a ~> {b}) -> (a -> UK g {b})
kra : (a -> UK g {b}) -> (FK g a ~> {b})
-- kla and kra mirror leftAdjunct and rightAdjunct from Data.Functor.Adjunction.
-- The underlying Haskell type is a -> g b on both sides, so we can simply have:
kla = id
kra = id

沿着Simon C的Three的思路,让我们使用g作为特征monad,变压器将在其上构建。转换器将以某种方式合并另一个Hask monad的效果,m,我有时将其称为“基础monad”,遵循习惯的Haskell术语。
如果我们试图在FK gUK g之间挤压m,我们会遇到上面提到的第二个问题:我们需要Kleisli-g内函子,而不是Hask内函子。除了编造,别无他法。我的意思是,我们可以为函子定义一个函子(更具体地说,是两类内函子之间的函子),这将有望将m变成我们可以使用的东西。我将这个“更高”的函子称为HK g。将其应用于m应该会给予如下结果:

-- Keep in mind this is a Kleisli-g endofunctor.
HK g m : {a}                |-> {m a}
         f : {a} ~> {b}     |-> kmap f : {m a} ~> {m b} ~ m a -> g (m b)
-- This is the object mapping, taking functors to functors.
-- The morphism mapping maps natural transformations, a la Control.Monad.Morph:
         t : ∀x. m x -> n x |-> kmorph t : ∀x. {m x} ~> {n x} ~ ∀x. m x -> g (n x)
-- I won't use it explicitly, but it is there if you look for it.

克莱斯利上的克莱斯利

  • (注:前面是冗长的明确的废话。如果你赶时间,可以浏览到“总结”小节。)*

UK g . HK g m . FK g将是一个Hask内函子,与Three结构对应。我们进一步希望它是Hask上的单子。我们可以通过将HK g m设置为Kleisli-g类别上的monad来确保这一点。这意味着我们需要在Kleisli-g上找出fmapreturnjoin的对应项:

kmap : {a} ~> {b} |-> {m a} ~> {m b}
       (a -> g b)  ->  m a -> g (m b)

kreturn : {a} ~> {m a}
          a -> g (m a)

kjoin : {m (m a)} ~> {m a}
        m (m a) -> g (m a)

对于kreturnkjoin,让我们尝试最简单的方法:

kreturn :: (Monad g, Monad m) => a -> g (m a)
kreturn = return . return 

kjoin :: (Monad g, Monad m) => m (m a) -> g (m a)
kjoin = return . join

kmap有点复杂。fmap @m将给予m (g a)而不是g (m a),因此我们需要一种方法将g层拉到外面。有一种方便的方法可以做到这一点,但它要求ga Distributive functor

kmap :: (Monad g, Distributive g, Monad m) => (a -> g b)  ->  m a -> g (m b)
kmap f = distribute . fmap f  -- kmap = collect

定律和分布性条件

当然,这些猜测毫无意义,除非我们能证明它们是合法的:

-- Functor laws for kmap
kmap return = return
kmap g <=< kmap f = kmap (g <=< f)

-- Naturality of kreturn
kmap f <=< kreturn = kreturn <=< f

-- Naturality of kjoin
kjoin <=< kmap (kmap f) = kmap f <=< kjoin

-- Monad laws
kjoin <=< kreturn = return
kjoin <=< kmap kreturn = return
kjoin <=< kmap kjoin = kjoin <=< kjoin

计算表明,composing monads with a distributive law的四个条件足以确保定律成立:

-- dist :: t (g a) -> g (t a)
-- I'm using `dist` instead of `distribute` and `t` instead of `m` here for the
-- sake of notation neutrality. 
dist . fmap (return @g) = return @g                 -- #1
dist . return @t = fmap (return @t)                 -- #2
dist . fmap (join @g) = join @g . fmap dist . dist  -- #3
dist . join @t = fmap (join @t) . dist . fmap dist  -- #4
-- In a nutshell: dist must preserve join and return for both monads.

在我们的例子中,条件#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:

HK g m = UHK g m . FHK g m

FHK g m : {a}        |-> <{a}>
      f : {a} ~> {b} |-> fmap return . f : <{a}> ~> <{b}> ~ a -> g (m b)
-- kreturn <=< f = fmap (return @m) . f
-- Note that m goes on the inside, so that we end up with a morphism in Kleisli g.

UHK g m : <{a}>          |-> {m a}
      f : <{a}> ~> <{b}> |-> fmap join . distribute . fmap f : {m a} ~> {m b} ~ m a -> g (m b)
-- kjoin <=< kmap f = fmap (join @m) . distribute . fmap f

-- The adjunction isomorphism:
hkla : (FHK g m {a} ~> <{b}>) -> ({a} ~> UHK g m <{b}>)
hkra : ({a} ~> UHK g m <{b}>) -> (FHK g m {a} ~> <{b}>)
-- Just like before, we have:
hkla = id
hkra = id

-- And, for the sake of completeness, a Kleisli composition operator:
-- g <~< f = kjoin <=< kmap g <=< f
(<~<) :: (Monad g, Distributive g, Monad m)
    => (b -> g (m c)) -> (a -> g (m b)) -> (a -> g (m c))
g <~< f = fmap join . join . fmap (distribute . fmap g) . f

现在我们手头有两个附加,我们可以组合它们,导致变压器附加,最后,变压器的returnjoin

-- The composition of the three morphism mappings in UK g . HK g m . FK g
-- tkmap f = join . fmap (kjoin <=< kmap (kreturn <=< return . f))
tkmap :: (Monad g, Distributive g, Monad m) => (a -> b) -> g (m a) -> g (m b)
tkmap = fmap . fmap

-- Composition of two adjunction units, suitably lifted through the functors.
-- tkreturn = join . fmap (hkla hkid) . kla kid = join . fmap kreturn . return
tkreturn :: (Monad g, Monad m) => a -> g (m a)
tkreturn = return . return

-- Composition of the adjunction counits, suitably lifted through the functors.
-- tkjoin = join . fmap (kjoin <=< kmap (hkra kid <~< (kreturn <=< kra id)))
--    = join . fmap (kjoin <=< kmap (return <~< (kreturn <=< id)))
tkjoin :: (Monad g, Distributive g, Monad m) => g (m (g (m a))) -> g (m a)
tkjoin = fmap join . join . fmap distribute

(For关于单位和计数单位的构成的范畴解释,见艾米丽Riehl,Category Theory In Context,命题4.4.4。

至于liftkmap (return @g)听起来像是一个合理的定义。这相当于distribute . fmap return(与来自Benjamin Hodgson's answer to Simon C's questionlift相比),根据条件#1,它简单地变为:

tklift :: m a -> g (m a)
tklift = return

MonadLift定律,即tklift必须是一个单子态射,确实成立,join定律依赖于分配性条件#1:

tklift . return = tkreturn
tklift . join = tkjoin . tkmap tklift . tklift

总结

Kleisli附加函数允许我们从任何Distributive单子构造一个变换子,方法是在任何其他单子的外部组合它。把所有这些放在一起,我们有:

-- This is still a Three, even though we only see two Hask endofunctors.
-- Or should we call it FourK?
newtype ThreeK g m a = ThreeK { runThreeK :: g (m a) }

instance (Functor g, Functor m) => Functor (ThreeK g m) where
    fmap f (ThreeK m) = ThreeK $ fmap (fmap f) m

instance (Monad g, Distributive g, Monad m) => Monad (ThreeK g m) where
    return a = ThreeK $ return (return a)
    m >>= f = ThreeK $ fmap join . join . fmap distribute 
        $ runThreeK $ fmap (runThreeK . f) m

instance (Monad g, Distributive g, Monad m) => Applicative (ThreeK g m) where
    pure = return
    (<*>) = ap

instance (Monad g, Distributive g) => MonadTrans (ThreeK g) where
    lift = ThreeK . return

Distributive的典型例子是函子。在另一个monad的外部组合它会得到ReaderT

newtype KReaderT r m a = KReaderT { runKReaderT :: r -> m a }
    deriving (Functor, Applicative, Monad) via ThreeK ((->) r) m
    deriving MonadTrans via ThreeK ((->) r)

ThreeK示例与规范的ReaderT示例完全一致。

翻转变压器和Eilenberg-Moore附加

在上面的推导中,我们将基础单子Klesli附接堆叠在特征单子附接之上。我们也可以反过来做,从基础单子的附加开始。在定义kmap时会发生关键的变化。由于基本单子原则上可以是任何单子,我们不想给它加上一个Distributive约束,这样它就可以被向外拉,就像我们在上面的推导中对g所做的那样。更适合我们的游戏计划的是,双重地,需要来自功能monad的Traversable,以便可以将其与sequenceA一起推入内部。这将导致一个变压器组成的feture单子的内部,而不是在外面。
下面是整体特征的内部结构。我称之为ThreeEM,因为它也可以通过使用Eilenberg-Moore附加(而不是Kleisli)并将它们与顶部的基础单子堆叠在一起来获得,就像Simon C的Three一样。这一事实可能与艾伦伯格-摩尔附加语和克莱西里附加语之间的二元性有关。

newtype ThreeEM t m a = ThreeEM { runThreeEM :: m (t a) }

instance (Functor t, Functor m) => Functor (ThreeEM t m) where
    fmap f (ThreeEM m) = ThreeEM $ fmap (fmap f) m

instance (Monad t, Traversable t, Monad m) => Monad (ThreeEM t m) where
    return a = ThreeEM $ return (return a)
    m >>= f = ThreeEM $ fmap join . join . fmap sequenceA 
      $ runThreeEM $ fmap (runThreeEM . f) m

instance (Monad t, Traversable t, Monad m) => Applicative (ThreeEM t m) where
    pure = return
    (<*>) = ap

-- In terms of of the Kleisli construction: as the bottom adjunction is now the
-- base monad one, we can use plain old fmap @m instead of kmap to promote return. 
instance (Monad t, Traversable t) => MonadTrans (ThreeEM t) where
    lift = ThreeEM . fmap return

以这种方式出现的常见变压器包括MaybeTExceptT
这种结构有一个潜在的缺陷。sequenceA必须遵循分布性条件,以便示例是合法的。然而,它的Applicative约束使得它的自然属性比distribute的自然属性弱得多,因此这些条件并不都是免费的:

  • 条件#1确实成立:它是Traversable的恒等式和自然律的结果。
  • #20002;的情况下,不能保证。sequenceA保留可遍历函子上的自然变换,只要这些变换保留toList。虽然return是这样的,但当被视为Identity的自然转换时,在许多常见情况下,它不是给定的。以这种方式出现的一个反例是Proxy / Const ()
  • #3也不能保证。如果将join @m作为Compose m m的自然变换,保留了(<*>),则它将成立,但情况可能并非如此。如果sequenceA实际上对效果进行了排序(也就是说,如果可遍历对象可以包含多个值),则join(<*>)在基本单子中执行的顺序所产生的任何差异都将导致违反条件。顺便说一句,这是臭名昭著的“ListT做错了”问题的一部分:根据这种构造构建的变压器中的ListT仅在与交换基单子一起使用时才是合法的。
  • 最后,条件#4仅在join @t(作为Compose t t的自然转换)保留toList时成立(即,如果它不删除,复制或重新排列元素)。一个结果是,这种构造对于join“取嵌套结构的对角线”的特征单子不起作用(通常情况下,单子也是Distributive示例),即使我们试图通过将自己限制在可交换的基单子上来掩盖条件#3。

这些限制意味着这种结构并不像人们希望的那样广泛适用。最后,Traversable的限制太宽泛了。我们真正需要的可能是将特征monad作为仿射可遍历对象(即,最多容纳一个元素的容器--参见this post by Oleg Grenrus了解一些镜头风格的讨论);据我所知,没有规范的Haskell类。

其他可能性

到目前为止所描述的构造要求特征单子分别为DistributiveTraversable。然而,总体策略并不是克莱斯利和艾伦伯格-摩尔附加语所特有的,所以可以想象在使用其他附加语的同时尝试它。通过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和它产生变压器的第三个附加函数呢?虽然我还没有详细地计算出来,但我怀疑把distributesequenceA(在这里的结构中使用的)分别认为属于右伴随和左伴随,而不是整个特征单子更合适。在distribute的情况下,这相当于超越了Haskell类型签名。

distribute :: (Distribute g, Functor m) => m (g a) -> g (m a)

...查看Kleisli-g-to-Hask函子之间的自然转换:

distribute  : m . UK g |-> UK g . HK g m

如果我是对的,那么就有可能扭转这个答案,并根据特征单子的Kleisli附加来重新解释Three/AdjointT结构。如果是这样的话,State并没有告诉我们很多关于其他既不是Distributive也不是Traversable的特征monad的信息。

ListT做对了

同样值得注意的是,并非所有的转换都是通过这里所看到的附加成分的合成来混合一元效果的。在 transformers 中,ContT和[SelectT不遵循模式;然而,我想说它们太古怪了,不能在这个上下文中讨论(“不是monads类别上的函子”,正如文档所指出的那样)。一个更好的例子是各种“ListT done right”实现,它通过以一种不需要在转换器的绑定中对它们进行排序的方式对基本单子效应进行网格化,避免了与sequenceA相关的非法问题(以及流丢失问题)。出于说明的目的,这里是实现的草图:

-- A recursion-schemes style base functor for lists.
data ListF a b = Nil | Cons a b
    deriving (Eq, Ord, Show, Functor)

-- A list type might be recovered by recursively filling the functorial
-- position in ListF.
newtype DemoList a = DemoList { getDemoList :: ListF a (DemoList a) }

-- To get the transformer, we compose the base monad on the outside of ListF.
newtype ListT m a = ListT { runListT :: m (ListF a (ListT m a)) }
    deriving (Functor, Applicative, Alternative) via WrappedMonad (ListT m)

-- Appending through the monadic layers. Note that mplus only runs the effect
-- of the first ListF layer; everything eslse can be consumed lazily.
instance Monad m => MonadPlus (ListT m) where
    mzero = ListT $ return Nil
    u `mplus` v = ListT $ runListT u >>= \case
        Nil -> runListT v
        Cons a u' -> return (Cons a (u' `mplus` v))

-- The effects are kept apart, and can be consumed as they are needed.
instance Monad m => Monad (ListT m) where
    return a = ListT $ pure (Cons a mzero)
    u >>= f = ListT $ runListT u >>= \case
        Nil -> return Nil
        Cons a v -> runListT $ f a `mplus` (v >>= f)

instance MonadTrans ListT where
    lift m = ListT $ (\a -> Cons a mzero) <$> m

在这个ListT中,基本单子效应既不在列表的内部也不在列表的外部。相反,它们被固定在列表的 Backbone.js 上,通过根据ListF定义类型来使它们变得有形。
以类似方式构建的相关转换器包括free-monad转换器FreeT,以及来自有效流库的核心monad转换器(我上面包含的“ListT done right”链接指向 pipes 文档并非巧合)。
这种转换器是否与这里描述的附加堆叠策略有某种联系?我还没有仔细考虑过这件事,所以没有说出来。这似乎是个值得深思的问题。

相关问题