31

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

标准技巧（在haskell-cafe post中向我建议）是包装Set到延续单子中。ContT不关心底层类型函子是否有任何约束。Set仅当将s 包装/展开到/从延续中时才需要约束：

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操作都是在最后执行的，而不是在每次单子计算之后执行。结果是只在最后Set构造和编辑了成倍增加的 s ，这对于大多数任务来说是不可接受的。union

有什么办法可以使这种建设高效吗？我试过但没有成功。

（我什至怀疑 Curry-Howard 同构和Glivenko 定理可能存在某种理论限制。Glivenko 定理说，对于任何命题重言式φ，公式¬¬φ都可以在直觉逻辑中得到证明。但是，我怀疑证明的长度（以正常形式）可以成倍地增长。所以，也许，将计算包装到延续单子中会使它成倍地增长？）

4

4 回答 4

21

单子是结构化和排序计算的一种特殊方式。monad 的绑定不能神奇地重组您的计算，以便以更有效的方式发生。构建计算的方式存在两个问题。

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

    也许这里的一些记忆会有所帮助。

  2. 一个更大的问题是对ContT计算结构的影响。通过一些等式推理，扩展 的结果replicate 20 step，定义foldrM并尽可能多地简化，我们可以看到它stepN 20 0等价于：

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

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

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

    我们看到，在评估(>>=)左侧的关联链时，每个绑定都会将新的计算推送到当前的 continuation 上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其余部分，即出现的右侧的所有内容。这意味着在每一步，我们都将剩余的计算捕获为，并应用与 中的元素一样多的次数。这些计算不像以前那样是基本的，而是组合的，这些计算将被重复很多次。setBindffset

问题的症结在于，ContTmonad 转换器正在将计算的初始结构（您的意思是setBind's 的左关联链）转换为具有不同结构的计算，即右关联链。毕竟这完全没问题，因为单子定律之一说，对于每个，m我们有fg

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

然而，单子定律并没有强制每个定律方程的每一侧的复杂性保持相同。事实上，在这种情况下，构建这种计算的左关联方式要高效得多。's的左关联链setBind立即计算，因为只有基本的子计算被复制。

事实证明，其他强行Set插入 monad 的解决方案也遇到了同样的问题。特别是set-monad包，产生类似的运行时。原因是它也将左关联表达式重写为右关联表达式。

我认为您已经指出了一个非常重要但相当微妙的问题，即坚持Set遵守Monad接口。而且我认为它无法解决。问题是monad的绑定类型需要是

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

a即在任何一个或上都不允许有类约束b。这意味着我们不能在左边嵌套绑定，除非首先调用 monad 法则来重写为右关联链。原因如下：给定(m >>= f) >>= g，计算的类型(m >>= f)为m b. 计算值(m >>= f)的类型为b。但是因为我们不能将任何类约束挂在类型变量上b，我们无法知道我们得到的值是否满足Ord约束，因此不能将此值用作我们希望能够计算的集合的元素union的。

于 2012-08-30T14:50:17.820 回答
11

最近在 Haskell Cafe Oleg 上给出了一个如何Set有效地实现 monad 的例子。报价：

...然而，高效的真正 Set monad 是可能的。

... 随附的是高效的正版 Set monad。我以直接的方式写了它（无论如何，它似乎更快）。关键是尽可能使用优化的选择功能。

  {-# LANGUAGE GADTs, TypeSynonymInstances, FlexibleInstances #-}

  module SetMonadOpt where

  import qualified Data.Set as S
  import Control.Monad

  data SetMonad a where
      SMOrd :: Ord a => S.Set a -> SetMonad a
      SMAny :: [a] -> SetMonad a

  instance Monad SetMonad where
      return x = SMAny [x]

      m >>= f = collect . map f $ toList m

  toList :: SetMonad a -> [a]
  toList (SMOrd x) = S.toList x
  toList (SMAny x) = x

  collect :: [SetMonad a] -> SetMonad a
  collect []  = SMAny []
  collect [x] = x
  collect ((SMOrd x):t) = case collect t of
                           SMOrd y -> SMOrd (S.union x y)
                           SMAny y -> SMOrd (S.union x (S.fromList y))
  collect ((SMAny x):t) = case collect t of
                           SMOrd y -> SMOrd (S.union y (S.fromList x))
                           SMAny y -> SMAny (x ++ y)

  runSet :: Ord a => SetMonad a -> S.Set a
  runSet (SMOrd x) = x
  runSet (SMAny x) = S.fromList x

  instance MonadPlus SetMonad where
      mzero = SMAny []
      mplus (SMAny x) (SMAny y) = SMAny (x ++ y)
      mplus (SMAny x) (SMOrd y) = SMOrd (S.union y (S.fromList x))
      mplus (SMOrd x) (SMAny y) = SMOrd (S.union x (S.fromList y))
      mplus (SMOrd x) (SMOrd y) = SMOrd (S.union x y)

  choose :: MonadPlus m => [a] -> m a
  choose = msum . map return


  test1 = runSet (do
    n1 <- choose [1..5]
    n2 <- choose [1..5]
    let n = n1 + n2
    guard $ n < 7
    return n)
  -- fromList [2,3,4,5,6]

  -- Values to choose from might be higher-order or actions
  test1' = runSet (do
    n1 <- choose . map return $ [1..5]
    n2 <- choose . map return $ [1..5]
    n  <- liftM2 (+) n1 n2
    guard $ n < 7
    return n)
  -- fromList [2,3,4,5,6]

  test2 = runSet (do
    i <- choose [1..10]
    j <- choose [1..10]
    k <- choose [1..10]
    guard $ i*i + j*j == k * k
    return (i,j,k))
  -- fromList [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]

  test3 = runSet (do
    i <- choose [1..10]
    j <- choose [1..10]
    k <- choose [1..10]
    guard $ i*i + j*j == k * k
    return k)
  -- fromList [5,10]

  -- Test by Petr Pudlak

  -- First, general, unoptimal case
  step :: (MonadPlus m) => Int -> m Int
  step i = choose [i, i + 1]

  -- repeated application of step on 0:
  stepN :: Int -> S.Set Int
  stepN = runSet . f
    where
    f 0 = return 0
    f n = f (n-1) >>= step

  -- it works, but clearly exponential
  {-
  *SetMonad> stepN 14
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
  (0.09 secs, 31465384 bytes)
  *SetMonad> stepN 15
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]
  (0.18 secs, 62421208 bytes)
  *SetMonad> stepN 16
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
  (0.35 secs, 124876704 bytes)
  -}

  -- And now the optimization
  chooseOrd :: Ord a => [a] -> SetMonad a
  chooseOrd x = SMOrd (S.fromList x)

  stepOpt :: Int -> SetMonad Int
  stepOpt i = chooseOrd [i, i + 1]

  -- repeated application of step on 0:
  stepNOpt :: Int -> S.Set Int
  stepNOpt = runSet . f
    where
    f 0 = return 0
    f n = f (n-1) >>= stepOpt

  {-
  stepNOpt 14
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14]
  (0.00 secs, 515792 bytes)
  stepNOpt 15
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15]
  (0.00 secs, 515680 bytes)
  stepNOpt 16
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16]
  (0.00 secs, 515656 bytes)

  stepNOpt 30
  fromList [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30]
  (0.00 secs, 1068856 bytes)
  -}
于 2013-05-13T12:36:01.240 回答
2

我不认为你在这种情况下的性能问题是由于使用Cont 

step' :: Int -> Set Int
step' i = fromList [i,i + 1]

foldrM' f z0 xs = Prelude.foldl f' setReturn xs z0
  where f' k x z = f x z `setBind` k

stepN' :: Int -> Int -> Set Int
stepN' times start = foldrM' ($) start (replicate times step')

Cont获得与基于实现类似的性能，但完全发生在Set“受限单子”中

我不确定我是否相信你关于 Glivenko 定理导致（标准化）证明大小呈指数增长的说法——至少在按需调用的情况下。那是因为我们可以任意重用子证明（而且我们的逻辑是二阶的，我们只需要 的一个证明forall a. ~~(a \/ ~a)）。证明不是树，它们是图（共享）。

通常，您可能会看到Cont包装带来的性能成本，Set但通常可以通过以下方式避免它们

smash :: (Ord r, Ord k) => SetM r r -> SetM k r
smash = fromSet . toSet
于 2012-08-29T23:29:14.343 回答
1

我发现了另一种可能性，基于 GHC 的ConstraintKinds扩展。这个想法是重新定义Monad，使其包含对允许值的参数约束：

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RebindableSyntax #-}

import qualified Data.Foldable as F
import qualified Data.Set as S
import Prelude hiding (Monad(..), Functor(..))

class CFunctor m where
    -- Each instance defines a constraint it valust must satisfy:
    type Constraint m a
    -- The default is no constraints.
    type Constraint m a = ()
    fmap   :: (Constraint m a, Constraint m b) => (a -> b) -> (m a -> m b)
class CFunctor m => CMonad (m :: * -> *) where
    return :: (Constraint m a) => a -> m a
    (>>=)  :: (Constraint m a, Constraint m b) => m a -> (a -> m b) -> m b
    fail   :: String -> m a
    fail   = error

-- [] instance
instance CFunctor [] where
    fmap = map
instance CMonad [] where
    return  = (: [])
    (>>=)   = flip concatMap

-- Set instance
instance CFunctor S.Set where
    -- Sets need Ord.
    type Constraint S.Set a = Ord a
    fmap = S.map
instance CMonad S.Set where
    return  = S.singleton
    (>>=)   = flip F.foldMap

-- Example:

-- prints fromList [3,4,5]
main = print $ do
    x <- S.fromList [1,2]
    y <- S.fromList [2,3]
    return $ x + y

（这种方法的问题在于单子值是函数的情况，例如m (a -> b)，因为它们不能满足像 一样的约束。所以对于这个受约束的单子，Ord (a -> b)不能使用<*>（或）这样的组合子。）apSet

于 2013-06-13T21:28:31.360 回答