使用continuation monad在`Set`(以及具有约束的其他容器)上构造有效的monad实例

Question

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

标准技巧(在haskell-cafe帖子中向我建议)是包含Set在延续monad中.ContT并不关心底层类型仿函数是否有任何约束.只有在将Sets 包装/展开到continuation中时才需要约束:

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操作都在最后执行,而不是在每次monadic计算之后执行它们.结果是指数多个Sets union仅在最后构造和编辑,这对于大多数任务来说是不可接受的.

有什么方法可以使这种结构高效吗？我试过但没有成功.

(我甚至怀疑,有可能是某些类型的从咖喱霍华德同构和下面的理论极限Glivenko定理.Glivenko定理说,对于任何命题同义反复φ公式¬¬φ可以在直觉逻辑来证明.但是,我怀疑证明的长度(以正常形式)可以是指数长的.因此,也许,可能存在将计算包装到延续monad中会使指数更长的情况？)

Answer 1

Monads是结构化和排序计算的一种特殊方式.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)
   

   我们看到,当评估一个(>>=)关联到左边的链时,每个绑定都会将一个新的计算推送到当前的连续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.计算不像以前那样基本,而是组合,并且这些计算将被重复多次.

问题的关键在于ContTmonad变换器正在将计算的初始结构(即您的左关联链)setBind转换为具有不同结构的计算,即右关联链.毕竟这是完全正常的,因为单子法律人说,对于每一个m,f和g我们有

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

然而,monad定律并未强调每个定律的方程式的每一侧的复杂性都是相同的.实际上,在这种情况下,构造此计算的左关联方式更有效.setBind's 的左关联链很快就会计算,因为只有基本的子计算是重复的.

事实证明,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的.

Answer 2

最近在Haskell Cafe Oleg举例说明了如何有效地实现Setmonad.引用:

......然而,高效的真正的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)
  -}