14

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

这让我思考是否有这样的事情MonadPlus。Codensitymonad 仅对 monadic 操作提高渐近性能，对mplus.

此外，虽然曾经有Control.MonadPlus.Free，但它已被删除以支持FreeT f []. 而且由于没有明确的 free MonadPlus，我不确定如何表达相应的improve变体。也许像

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

?

更新：我尝试使用回溯LogicTmonad 创建这样的 monad，它似乎以类似于以下方式定义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

但是，它有些不对劲，从我最初的实验看来，对于某些示例，k它与improvePlus k. 我不确定，如果这是一个基本的限制，LogicT并且需要一个不同的、更复杂的 monad，或者只是我lowerLogic错误地定义（或其他东西）。

4

1 回答 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 ：

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 (endo)functor f，我们可以构造自由的 monad Free f，它会遇到与左嵌套绑定类似的性能问题，以及使用 Cayley 表示的类似解决方案 Codensity。

Near-semirings 而不仅仅是幺半群

这就是本文停止回顾工作中的 Haskell 程序员所熟知的概念的地方，并开始关注其目标。Near-semiring 就像一个环，除了更简单，因为加法和乘法都只需要是幺半群。这两个操作之间的联系是您所期望的：

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

自由的近半边（over 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]e 在 endomorphisms 上获得 endomorphisms 的半环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两次该结构）。当我们概括这一点时，这两层将不一样。论文接着说：

请注意，这不是从intorep的近半同态， 因为它不保留单位 [...] 然而，[...] 如果我们将值提升到表示形式，则在近半半上计算的语义将被保留，在那里进行近半运算，然后回到原来的近半运算。NDC(N)

MonadPlus几乎是半成品

然后论文继续重新定义MonadPlus类型类，使其符合近乎半规则：(mzero, mplus)是单曲面的：

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

它与预期的 monad-monoid 交互：

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

或者，使用绑定：

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

但是，这些不是现有MonadPlus typeclass from base的规则，它们被列为：

mzero >>= _  =  mzero
_ >> mzero   =  mzero

该论文将MonadPlus满足近似半规则的实例称为“非确定性单子”，并引用Maybe了一个MonadPlus但不是非确定性单子的示例，因为设置m1 = Just Nothing和m2 = Just (Just False)是 的反例join (m1 `mplus` m2) = join m1 `mplus` join m2。

非确定性单子的自由和凯莱表示

把所有东西放在一起，一方面我们有Forest-like free nondeterminism monad：

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)

另一方面，两个 monoidal 层的双 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)

立即返回。

于 2015-09-01T13:56:28.653 回答