haskell - 使用延续monad在 `Set`(和其他具有约束的容器)上构造有效的monad实例

Question

Set与[]类似，具有完美定义的monadic操作。问题在于它们要求值满足Ord约束，因此，没有任何约束就无法定义return和>>=。同样的问题也适用于许多其他数据结构，这些结构需要对可能的值进行某种约束。

标准技巧(在haskell-cafe post中向我建议)是将Set包装到延续monad中。 ContT不在乎基础类型函子是否具有任何约束。仅当将Set包装到延续中或从延续中解包时，才需要约束:

import Control.Monad.Cont
import Data.Foldable (foldrM)
import Data.Set

setReturn :: a -> Set a
setReturn = singleton

setBind :: (Ord b) => Set a -> (a -> Set b) -> Set b
setBind set f = foldl' (\s -> union s . f) empty set

type SetM r a = ContT r Set a

fromSet :: (Ord r) => Set a -> SetM r a
fromSet = ContT . setBind

toSet :: SetM r r -> Set r
toSet c = runContT c setReturn

这可以根据需要工作。例如，我们可以模拟一个不确定性函数，该函数要么将其参数增加1，要么使其完整无缺:

step :: (Ord r) => Int -> SetM r Int
step i = fromSet $ fromList [i, i + 1]

-- repeated application of step:
stepN :: Int -> Int -> Set Int
stepN times start = toSet $ foldrM ($) start (replicate times step)

实际上，stepN 5 0产生fromList [0,1,2,3,4,5]。如果我们改用[] monad，我们将得到

[0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5]

代替。

问题是效率。如果我们调用stepN 20 0，则输出将花费几秒钟，并且stepN 30 0在合理的时间内无法完成。事实证明，所有Set.union操作都在最后执行，而不是在每次单子(monad)计算之后执行。结果是，仅在最后以指数方式构造了许多Set并对其进行了union编码，这对于大多数任务而言是 Not Acceptable 。

有没有办法解决这个问题？我尝试了但没有成功。

(我什至怀疑Curry-Howard同构和Glivenko's theorem可能会有一些理论上的限制。格里芬科定理说，对于任何命题重言式φ¬¬φ都能在直觉逻辑中得到证明。但是，我怀疑长度证明的形式(标准形式)可能会成倍增长。因此，也许在某些情况下，将计算包装到延续单子(monad)中会使其成倍增长？)

Answer 1

Monad是结构化和排序计算的一种特殊方式。 monad的绑定(bind)无法神奇地重组您的计算，从而以更有效的方式进行计算。结构化计算方式存在两个问题。

在评估stepN 20 0时，step 0的结果将被计算20次。这是因为计算的每个步骤都会产生0作为一个替代项，然后将其馈送到下一步，该步骤也会产生0作为替代项，依此类推...

也许此处的一些备忘会有所帮助。

一个更大的问题是ContT对您的计算结构的影响。通过一些方程式推理，扩展了replicate 20 step的结果，foldrM的定义并根据需要进行了多次简化，我们可以看到stepN 20 0等效于:

(...(return 0 >>= step) >>= step) >>= step) >>= ...)

该表达式的所有括号都在左侧。很好，因为这意味着每次出现(>>=)的RHS都是一个基本计算，即step，而不是组成的计算。但是，放大(>>=)的ContT定义，

m >>= k = ContT $ \c -> runContT m (\a -> runContT (k a) c)

我们看到，在评估与左侧关联的(>>=)链时，每个绑定(bind)会将新的计算推入当前的延续c。为了说明发生了什么，我们可以再次使用一些方程式推理，将(>>=)的定义和runContT的定义扩展开，然后简化并得出:

setReturn 0 `setBind`
    (\x1 -> step x1 `setBind`
        (\x2 -> step x2 `setBind` (\x3 -> ...)...)

现在，对于每次出现的setBind，我们都要问自己RHS参数是什么。对于最左边的出现，RHS参数是setReturn 0之后的整个计算的其余部分。对于第二次出现，它是step x1等之后的所有内容。让我们放大到setBind的定义:

setBind set f = foldl' (\s -> union s . f) empty set

这里f代表所有其余的计算，所有内容都在setBind出现的右侧。这意味着在每一步中，我们将其余的计算捕获为f，并应用f的次数与set中存在的元素的次数相同。计算不像以前那样基本，而是组成的，这些计算将被重复很多次。

问题的症结在于ContT monad转换器将计算的初始结构(即setBind的左关联链)转换为具有不同结构的计算，即右关联链。毕竟这是完全可以的，因为单子(monad)法则之一说，对于每个m，f和g

(m >>= f) >>= g = m >>= (\x -> f x >>= g)

但是，莫纳德定律并不意味着每个定律的方程式的每一边都具有相同的复杂度。的确，在这种情况下，构造此计算的左关联方式效率更高。 setBind的左侧关联链不会立即求值，因为只复制了基本子计算。

事实证明，将Set编码为monad的其他解决方案也存在相同的问题。特别是，set-monad包产生了类似的运行时。原因是它也将左联想表达式重写为右联想表达式。

我认为您已将放在非常重要但相当微妙的问题上，坚持要求Set遵循Monad接口(interface)。而且我认为这无法解决。问题是单子(monad)绑定(bind)的类型需要为

(>>=) :: m a -> (a -> m b) -> m b

即，不允许对a或b进行类约束。这意味着我们无法在左侧嵌套绑定(bind)，而无需先调用monad定律来重写为右侧的关联链。原因如下:给定(m >>= f) >>= g，计算(m >>= f)的类型为m b。计算(m >>= f)的值为b类型。但是，因为我们无法将任何类约束都卡在类型变量b上，所以我们无法知道所获得的值满足Ord约束，因此无法将此值用作我们希望能够在其上使用的集合的元素计算union。