伴随函子决定单子变换器,但提升在哪里?

Adjoint functors determine monad transformers, but where's lift?

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

{-# 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

非常酷,但我对一些事情感到困惑:

How can we upgrade a monadic m a into a monadic 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))。这是 distribute if g is Distributive.

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 = _

由于我们需要 return 一个 gAdjunction 中明确选择的方法是 leftAdjunct :: Adjunction f g => (f a -> b) -> a -> g b,它使用 unit 创建一个 g (f a) 然后通过 fmapping 一个函数来拆除内部 f a

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

这个推导可能看起来像一个魔术,但实际上你只是通过练习才能更好地打网球。游戏的技巧是能够查看类型并应用关于您正在使用的对象的直觉和事实。通过查看类型,我可以看出我需要交换 mg,并且遍历 m 不是一个选项(因为 m 不一定是 Traversable), 所以像 distribute 这样的东西是必要的。

除了猜测我将需要实施 distribute 之外,我还得到了关于附加作用如何工作的一些常识的指导。

具体来说,当您谈论 * -> * 时,唯一有趣的附加词是(唯一同构的)Reader/Writer 附加词。特别是,这意味着 Hask 上的任何右伴随总是 Representable, as witnessed by tabulateAdjunction and indexAdjunction. I also know that all Representable functors are Distributive (in fact logically the converse is also true, as described in Distributive's docs, even though the classes aren't equivalent in power), per distributeRep.


For that matter, how can we upgrade g a into a Three g f m a (provided Adjoint f g)?

我会把它留作练习。我怀疑您需要再次依靠 g ~ ((->) s) 同构。我实际上不希望这个对所有的附加条件都是正确的,只是 Hask 上的那些,其中只有一个。

lift,在中设置为:

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

Edward Kmett's corresponding MonadTrans instanceTraversable 要求源于此。那么,问题就变成了是否像您所说的那样依赖 "cheating"。我要争辩说它不是。

我们可以采用本杰明关于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 告诉我们 unabsurdLcozipL 见证了“[a] 左伴随必须居留,[并且] 左伴随必须恰好由一个元素居留”,分别.然而,这意味着 splitL 精确对应于表征 Traversable 函子的 shape-and-contents 分解。如果我们加上 splitLunsplitL 是相反的事实,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 的两个实现是否等效。那并不难,只是有点费力。简而言之,这里的distributeRsequenceR定义可以简化为:

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——第二个 right-hand 方 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

要点是通往 MonadTransTraversable 路线与 Distributive 路线一样安全,并且担心它 - 包括 [= 提到的那些46=] 文档 -- 应该不会再麻烦任何人了。

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

lift = Three . leftAdjunct sequenceL

liftsequenceL通过adjunction同构发送。此外,来自...

leftAdjunct sequenceL = distributeR . fmap unit

...如果我们在两边应用rightAdjunct,我们会得到...

sequenceL = rightAdjunct (distributeR . fmap unit)

... 如果我们在两边的左边组成 fmap (fmap counit),我们最终会得到:

distributeR = leftAdjunct (fmap counit . sequenceL)

所以distributeRsequenceL可以相互定义。