伴随函子确定单子变换器，但升力在哪里？

Question

我对@9​​87654321@ 中描述的用于从伴随函子确定单子变换器的构造很感兴趣。下面是一些总结基本思想的代码：

{-# LANGUAGE MultiParamTypeClasses #-}

import           Control.Monad

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

class (Functor f, Functor g) => Adjoint f g where
  counit :: f (g a) -> a
  unit   :: a -> g (f a)

instance (Adjoint f g, Monad m) => Monad (Three g f m) where
  return  = Three . fmap return . unit
  m >>= f = Three $ fmap (>>= counit . fmap (getThree . f)) (getThree m)

instance (Adjoint f g, Monad m) => Applicative (Three g f m) where
  pure  = return
  (<*>) = ap

instance (Adjoint f g, Monad m) => Functor (Three g f m) where
  fmap = (<*>) . pure

鉴于Adjoint ((,) s) ((->) s)，Three ((->) s) ((,) s) 看起来等同于StateT s。

非常酷，但我对一些事情感到困惑：

• 我们如何将一个单子 m a 升级为一个单子 Three g f m a？对于Three ((->) s) ((,) s) 的具体情况，如何做到这一点当然很明显，但如果Adjoint f g 有一个适用于任何Three g f 的配方似乎是可取的。换句话说，似乎应该有一个lift 的类比，其定义只需要unit、counit，以及输入monad 的return 和>>=。但我似乎找不到（我见过a definition using sequence，但这似乎有点像作弊，因为它要求f 是Traversable）。

• 就此而言，我们如何将g a 升级为Three g f m a（提供Adjoint f g）？同样，对于Three ((->) s) ((,) s) 的具体情况，如何做到这一点很明显，但我想知道是否有类似的gets 只需要unit、counit，以及return 和>>=输入单子。

Answer 1

我们如何将一元 m a 升级为一元 Three g f m a？

好问题。是时候打一场网球比赛了！

-- i'm using Adjuction from the adjunctions package because I'll need the fundeps soon
lift :: Adjunction f g => m a -> Three g f m a
lift mx = Three _

孔的类型为g (m (f a))。我们有mx :: m a 在范围内，当然还有unit :: a -> g (f a) 和fmap :: (a -> b) -> m a -> m b。

lift mx = let mgfx = fmap unit mx
          in Three $ _ mgfx

现在是_ :: m (g (f a)) -> g (m (f a))。如果g 是Distributive，则这是distribute。

lift mx = let mgfx = fmap unit mx
              gmfx = distributeR mgfx
          in Three gmfx
-- or
lift = Three . distributeR . fmap unit

所以现在我们只需要证明一个附加词的右边总是Distributive：

distributeR :: (Functor m, Adjunction f g) => m (g x) -> g (m x)
distributeR mgx = _

由于我们需要返回一个g，所以从Adjunction 中明确选择的方法是leftAdjunct :: Adjunction f g => (f a -> b) -> a -> g b，它使用unit 创建一个g (f a)，然后通过@987654351 拆掉内部的f a @ping 一个函数。

distributeR mgx = leftAdjunct (\fa -> _) _

我将首先攻打第一个洞，期望填满它可能会告诉我关于第二个洞的一些信息。第一个孔的类型为m a。我们获得任何类型的m 的唯一方法是通过fmapping mgx。

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> _) mgx) _

现在第一个洞的类型是a，我们在范围内有gx :: g a。如果我们有f (g a)，我们可以使用counit。但我们确实有一个f x（其中x 当前是一个模棱两可的类型变量）和一个g a 在范围内。

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> counit (fa $> gx)) mgx) _

事实证明，剩下的洞有一个模棱两可的类型，所以我们可以使用任何我们想要的东西。 （$> 会忽略它。）

distributeR mgx = leftAdjunct (\fa -> fmap (\gx -> counit (fa $> gx)) mgx) ()

---

这种推导可能看起来像是魔术，但实际上你只是通过练习才能更好地打网球。游戏的技巧是能够查看类型并应用有关您正在使用的对象的直觉和事实。从查看类型我可以看出我将需要交换m 和g，并且遍历m 不是一种选择（因为m 不一定是Traversable），所以像@ 987654373@ 将是必要的。

除了猜测我将需要实现 distribute 之外，我还受到了一些关于附加功能如何工作的一般知识的指导。

具体来说，当您谈论 * -> * 时，唯一有趣的附加词是（唯一同构于）Reader/Writer 附加词。特别是，这意味着Hask 上的任何右伴随总是Representable，正如tabulateAdjunction 和indexAdjunction 所见证的那样。我也知道所有Representable 函子都是Distributive（事实上，反之亦然，如Distributive's docs 中所述，即使这些类的功率不相等），每个distributeRep。

---

就此而言，我们如何将g a 升级为Three g f m a（提供Adjoint f g）？

我将把它留作练习。我怀疑您需要再次依赖g ~ ((->) s) 同构。我实际上并不指望这个对所有的附属词都是正确的，只是Hask 上的那些，其中只有一个。

Answer 2

lift，在Benjamin Hodgson's answer中，设置为：

lift mx = let mgfx = fmap unit mx
              gmfx = distributeR mgfx
          in Three gmfx
-- or
lift = Three . distributeR . fmap unit

如您所知，这不是我们可能使用的唯一合理策略：

lift mx = let gfmx = unit mx
              gmfx = fmap sequenceL gfmx
          in Three gmfx
-- or
lift = Three . fmap sequenceL . unit

Traversable 对 Edward Kmett's corresponding MonadTrans instance 的要求从何而来。那么，问题就变成了，正如你所说，依赖它是否是“作弊”。我会争辩说不是。

我们可以调整Benjamin关于Distributive和右伴随的游戏计划，并尝试找出左伴随是否是Traversable。查看Data.Functor.Adjunction 表明我们有一个非常好的工具箱可供使用：

unabsurdL :: Adjunction f u => f Void -> Void
cozipL :: Adjunction f u => f (Either a b) -> Either (f a) (f b)
splitL :: Adjunction f u => f a -> (a, f ())
unsplitL :: Functor f => a -> f () -> f a

Edward 有用地告诉我们，unabsurdL 和 cozipL 分别见证了“[a] left adjoint 必须被居住，[and that] left adjoint 必须被恰好一个元素居住”。然而，这意味着splitL 恰好对应于表征Traversable 函子的形状和内容分解。如果我们再加上splitL 和unsplitL 是相反的事实，那么sequence 的实现就会立即出现：

sequenceL :: (Adjunction f u, Functor m) => f (m a) -> m (f a)
sequenceL = (\(mx, fu) -> fmap (\x -> unsplitL x fu) mx) . splitL

（请注意，m 的要求不超过 Functor，正如预期的那样，对于只包含一个值的可遍历容器。）

此时缺少的只是验证lift 的两个实现是否等效。这并不难，只是有点费力。简而言之，这里的distributeR 和sequenceR 定义可以简化为：

distributeR = \mgx ->
    leftAdjunct (\fa -> fmap (\gx -> rightAdjunct (const gx) fa) mgx) ()   
sequenceL =
    rightAdjunct (\mx -> leftAdjunct (\fu -> fmap (\x -> fmap (const x) fu) mx) ())

我们想证明distributeR . fmap unit = fmap sequenceL . unit。经过几轮简化后，我们得到：

distributeR . fmap unit = \mgx ->
    leftAdjunct (\fa -> fmap (\gx -> rightAdjunct (const (unit gx)) fa) mgx) ()
fmap sequenceL . unit = \mx ->
    leftAdjunct (\fu -> fmap (\x -> fmap (const x) fu) mx) ()

我们可以通过选择\fu -> fmap (\x -> fmap (const x) fu) mx（右侧第二个leftAdjunct 的参数）并将rightAdjunct unit = counit . fmap unit = id 滑入其中来证明它们实际上是同一件事：

\fu -> fmap (\x -> fmap (const x) fu) mx
\fu -> fmap (\x -> fmap (const x) fu) mx
\fu -> fmap (\x -> (counit . fmap unit . fmap (const x)) fu) mx
\fu -> fmap (\x -> rightAdjunct (unit . const x) fu) mx
\fu -> fmap (\x -> rightAdjunct (const (unit x)) fu) mx
-- Sans variable renaming, the same as
-- \fa -> fmap (\gx -> rightAdjunct (const (unit gx)) fa) mgx

要点是，通往您的MonadTrans 的Traversable 路由与Distributive 一样安全，并且对它的担忧——包括Control.Monad.Trans.Adjoint 文档中提到的那些——应该不再麻烦任何人。

P.S.：值得注意的是，这里提出的lift的定义可以拼写为：

lift = Three . leftAdjunct sequenceL

即lift是通过附加同构发送的sequenceL。此外，从...

leftAdjunct sequenceL = distributeR . fmap unit

...如果我们在两边都应用rightAdjunct，我们得到...

sequenceL = rightAdjunct (distributeR . fmap unit)

...如果我们在两边的左边写fmap (fmap counit)，我们最终会得到：

distributeR = leftAdjunct (fmap counit . sequenceL)

所以distributeR 和sequenceL 是可以相互定义的。