有一个Codensity MonadPlus可以渐进地优化一系列MonadPlus操作吗?

16

最近有一个关于DList <-> []Codensity <-> Free 之间关系的问题

这让我想到是否有类似于 MonadPlus 的东西。然而,Codensity monad 仅提高了单子操作的渐近性能,而不是 mplus

此外,虽然曾经有过 Control.MonadPlus.Free,但它已被移除,改用 FreeT f []。由于没有明确的自由 MonadPlus,我不确定如何表达相应的improve变量。也许可以尝试:

improvePlus :: Functor f => (forall m. (MonadFree f m, MonadPlus m) => m a) -> FreeT f [] a

更新:我尝试使用回溯LogicT单子创建这样的单子,它似乎以类似于Codensity的方式定义:

newtype LogicT r m a = LogicT { unLogicT :: forall r. (a -> m r -> m r) -> m r -> m r }

它适用于回溯计算,即MonadPlus

然后我定义了lowerLogic,类似于lowerCodensity,如下所示:

{-# LANGUAGE RankNTypes, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses,
             UndecidableInstances, DeriveFunctor #-}
import Control.Monad
import Control.Monad.Trans.Free
import Control.Monad.Logic

lowerLogic :: (MonadPlus m) => LogicT m a -> m a
lowerLogic k = runLogicT k (\x k -> mplus (return x) k) mzero

然后,补充相应的 MonadFree 实例。
instance (Functor f, MonadFree f m) => MonadFree f (LogicT m) where
    wrap t = LogicT (\h z -> wrap (fmap (\p -> runLogicT p h z) t))

可以定义

improvePlus :: (Functor f, MonadPlus mr)
            => (forall m. (MonadFree f m, MonadPlus m) => m a)
            -> FreeT f mr a
improvePlus k = lowerLogic k

然而,它似乎存在问题,从我的初始实验中可以看出,对于某些例子,kimprovePlus k 不同。我不确定这是否是 LogicT 的基本限制,需要使用不同的更复杂的单子,还是只是我错误地定义了 lowerLogic(或其他什么东西)。


5
论文与你的问题非常相关。该论文提供了对MonadPlus类型类操作的新代数理解,使我们能够得出自由结构和优化的Cayley式表示。 - Matthew Pickering
你能举个例子,说明在你实现的LogicT单子变换器中,什么情况下 kimprovePlus k 不同吗? - Aadit M Shah
1个回答

11
以下内容均基于Matthew Pickering在评论中发布的非常有趣的论文:从幺半群到近半环:MonadPlus和Alternative的本质 (E. Rivas, M. Jaskelioff, T. Schrijvers)。所有结论均为他们所得;所有错误均为我的。

从自由幺半群到DList

为了建立直觉,首先考虑Haskell类型范畴Hask上的自由幺半群[][] 的一个问题是,如果你有...
(xs `mappend` ys) `mappend` zs = (xs ++ ys) ++ zs

然后对此进行评估需要遍历和重新遍历xs,针对每个左嵌套的mappend应用。

解决方案是使用CPS,采用差分列表(difference lists)形式:

newtype DList a = DL { unDL :: [a] -> [a] }

本文考虑这个泛型形式(称为Cayley表示),在此我们不局限于自由幺半群:
newtype Cayley m = Cayley{ unCayley :: Endo m }

使用转换

toCayley :: (Monoid m) => m -> Cayley m
toCayley m = Cayley $ Endo $ \m' -> m `mappend` m'

fromCayley :: (Monoid m) => Cayley m -> m
fromCayley (Cayley k) = appEndo k mempty

泛化的两个方向

我们可以通过两种方式来泛化上述结构:第一种是考虑在Hask之外,而是在Hask的自函子上的幺半群;即单子;第二种是将代数结构丰富成近半环。

Free单子到Codensity

对于任何Haskell(自)函子f,我们可以构造出Free f 自由单子,它会有类似于左嵌套绑定的性能问题,使用Cayley表示Codensity的解决方案也是相似的。

近半环而不仅仅是幺半群

这里,本文停止审查对于熟悉 Haskell 的程序员而言已经众所周知的概念,开始聚焦于其目标。近半环类似于一个环,但更为简单,因为只需要加法和乘法是幺半群。两个操作之间的联系就像你预期的那样:
zero |*| a = zero
(a |+| b) |*| c = (a |*| c) |+| (b |*| c)

其中(zero, |+|)(one, |*|)是基于共享基础的两个单子:

class NearSemiring a where
    zero :: a
    (|+|) :: a -> a -> a
    one :: a
    (|*|) :: a -> a -> a

免费的近半环(在Hask上)实际上是以下Forest类型:

newtype Forest a = Forest [Tree a]
data Tree a = Leaf | Node a (Forest a)

instance NearSemiring (Forest a) where
    zero = Forest []
    one = Forest [Leaf]
    (Forest xs) |+| (Forest ys) = Forest (xs ++ ys)
    (Forest xs) |*| (Forest ys) = Forest (concatMap g xs)
      where
        g Leaf = ys
        g (Node a n) = [Node a (n |*| (Forest ys))]

很幸运我们没有交换或逆元,这使自由表示远非平凡...

然后,该论文对两个单调结构分别应用Cayley表示。

然而,如果我们这样做得太简单,我们将无法获得一个好的表示:我们想要表示一个“近环”,因此必须考虑整个“近环”结构,而不仅仅是一个选择的单体结构。[...] [W] 我们可以得到循环同态上的半环DC(N)

newtype DC n = DC{ unDC :: Endo (Endo n) }

instance (Monoid n) => NearSemiring (DC n) where
    f |*| g = DC $ unDC f `mappend` unDC g
    one = DC mempty
    f |+| g = DC $ Endo $ \h -> appEndo (unDC f) h `mappend` h
    zero = DC $ Endo $ const mempty

我稍微修改了这里的实现方式,强调我们使用了两次Endo结构。当我们将其推广时,这两个层次将不会相同。然后,论文继续说:

请注意,rep不是从NDC(N)的近半环同态,因为它没有保留单位元[...] 然而,如果我们将值提升到表示形式,进行近半环计算,然后回到原始近半环,计算过程的语义将得到保留。

MonadPlus几乎是一个近半环

然后,论文继续重新定义MonadPlus类型类,以便符合近半环规则:(mzero, mplus)是单子的:

m `mplus` mzero = m
mzero `mplus` m = m
m1 `mplus` (m2 `mplus` m3) = (m1 `mplus` m2) `mplus` m3

它与单子-幺半群的交互如预期一样:

join mzero = mzero
join (m1 `mplus` m2) = join m1 `mplus` join m2

或者,使用绑定:

mzero >>= _ = mzero
(m1 `mplus` m2) >>= k = (m1 >>= k) `mplus` (m2 >>= k)

然而,这些不是来自base现有的MonadPlus类型类规则,列举如下:
mzero >>= _  =  mzero
_ >> mzero   =  mzero

这篇论文将满足类似于近半环律的MonadPlus实例称为“非确定性单子”,并引用Maybe作为一个例子,它是MonadPlus但不是非确定性单子,因为设置m1 = Just Nothingm2 = Just (Just False)join (m1 `mplus` m2) = join m1 `mplus` join m2的反例。
另一方面,我们有类似于Forest的自由非确定性单子以及Cayley表示形式。
newtype FreeP f x = FreeP { unFreeP :: [FFreeP f x] }
data FFreeP f x = PureP x | ConP (f (FreeP f x))

instance (Functor f) => Functor (FreeP f) where
    fmap f x = x >>= return . f

instance (Functor f) => Monad (FreeP f) where
    return x = FreeP $ return $ PureP x
    (FreeP xs) >>= f = FreeP (xs >>= g)
      where
        g (PureP x) = unFreeP (f x)
        g (ConP x) = return $ ConP (fmap (>>= f) x)

instance (Functor f) => MonadPlus (FreeP f) where
    mzero = FreeP mzero
    FreeP xs `mplus` FreeP ys = FreeP (xs `mplus` ys)

另一方面,两个单调层的双Cayley表示:
newtype (:^=>) f g x = Ran{ unRan :: forall y. (x -> f y) -> g y }
newtype (:*=>) f g x = Exp{ unExp :: forall y. (x -> y) -> (f y -> g y) }

instance Functor (g :^=> h) where
    fmap f m = Ran $ \k -> unRan m (k . f)

instance Functor (f :*=> g) where
    fmap f m = Exp $ \k -> unExp m (k . f)

newtype DCM f x = DCM {unDCM :: ((f :*=> f) :^=> (f :*=> f)) x}

instance Monad (DCM f) where
    return x = DCM $ Ran ($x)
    DCM (Ran m) >>= f = DCM $ Ran $ \g -> m $ \a -> unRan (unDCM (f a)) g

instance MonadPlus (DCM f) where
    mzero = DCM $ Ran $ \k -> Exp (const id)
    mplus m n = DCM $ Ran $ \sk -> Exp $ \f fk -> unExp (a sk) f (unExp (b sk) f fk)
      where
        DCM (Ran a) = m
        DCM (Ran b) = n

caylize :: (Monad m) => m a -> DCM m a
caylize x = DCM $ Ran $ \g -> Exp $ \h m -> x >>= \a -> unExp (g a) h m

-- I wish I called it DMC earlier...
runDCM :: (MonadPlus m) => DCM m a -> m a
runDCM m = unExp (f $ \x -> Exp $ \h m -> return (h x) `mplus` m) id mzero
  where
    DCM (Ran f) = m

这篇论文举了一个在非确定性单子中运行的计算示例,对于FreeP来说表现不佳。
anyOf :: (MonadPlus m) => [a] -> m a
anyOf [] = mzero
anyOf (x:xs) = anyOf xs `mplus` return x

事实上,尽管

length $ unFreeP (anyOf [1..100000] :: FreeP Identity Int)

需要很长时间,Cayley 变换后的版本

length $ unFreeP (runDCM $ anyOf [1..100000] :: FreeP Identity Int)

立即返回。


似乎 LogicT Monad 转换器已足够支持高效的 MonadPlus 操作,而不需要 DCM 的复杂性。特别地,我们可以将 :*=> newtype 重新定义为 newtype (:*=>) f g x = Exp { unExp :: f x -> g x },并相应更新其余代码,所有东西仍能如预期般运行。这是因为在当前的 Exp 定义中,(x -> y) 端态映射是不必要的。在 runDCM 的定义中,我们只提供了 id 这一类型的值。 - Aadit M Shah

网页内容由stack overflow 提供, 点击上面的
可以查看英文原文,
原文链接