Построение эффективных экземпляров монады в `Set` (и других контейнерах с ограничениями) с использованием продолжения монады

Set, аналогично [] имеет совершенно определенные монадические операции. Проблема в том, что они требуют, чтобы значения удовлетворяли условию Ord, и поэтому невозможно определить return и >>= без каких-либо ограничений. Эта же проблема применяется ко многим другим структурам данных, которые требуют каких-либо ограничений на возможные значения.

Стандартный трюк (предложенный мне в статье haskell-cafe) заключается в том, чтобы обернуть Set в монаду продолжения. 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]. Если бы мы использовали вместо монады [], мы получили бы

[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 построены и union ed только в конце, что неприемлемо для большинства задач.

Есть ли способ обойти это, чтобы сделать эту конструкцию эффективной? Я пробовал, но безуспешно.

(Я даже подозреваю, что могут существовать некоторые теоретические пределы, вытекающие из изоморфизма Карри-Говарда и теоремы Гливенко. Теорема Гливенко гласит, что для любой пропозициональной тавтологии φ формула ¬¬φ может быть доказана в интуиционистской логике. Однако я подозреваю, что длина доказательства (в нормальной форме) может быть экспоненциально длинной. Поэтому, возможно, могут быть случаи, когда перенос вычисления в монаду продолжения сделает ее экспоненциально длиннее?)

Ответ 1

Монады - это один из способов структурирования и упорядочения вычислений. Связывание монады не может магически перестроить ваши вычисления, чтобы это произошло более эффективным образом. Есть две проблемы с тем, как вы структурируете свои вычисления.

При оценке 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)
```
мы видим, что при оценке цепи (>>=), связанной с левым, каждое связывание подталкивает новое вычисление к текущему продолжению 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 преобразует исходную структуру вычисления, которую вы имели в виду как левую ассоциативную цепочку setBind, в вычисление с другой структурой, то есть правая ассоциативная цепь. Все это прекрасно, потому что один из законов монады говорит, что для каждого m, f и g имеем

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

Однако законы монады не налагают, что сложность остается неизменной с каждой стороны уравнений каждого закона. И действительно, в этом случае левый ассоциативный способ структурирования этого вычисления намного эффективнее. Левая ассоциативная цепочка setBind мгновенно оценивается, потому что дублируются только элементарные подкомплексы.

Оказывается, что другие решения shoehorning set в монаду также страдают от одной и той же проблемы. В частности, пакет set-monad дает аналогичные версии. Причина в том, что он тоже переписывает левые ассоциативные выражения в правильные ассоциативные.

Я думаю, вы указали на очень важную, но довольно тонкую проблему, настаивая на том, что set подчиняется интерфейсу Monad. И я не думаю, что это можно решить. Проблема в том, что тип привязки монады должен быть

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

то есть ограничение класса не допускается ни на a, ни на b. Это означает, что мы не можем вложить привязки слева, не прибегая сначала к законам монады, чтобы переписать их в правую ассоциативную цепочку. Вот почему: при заданном (m >>= f) >>= g тип вычисления (m >>= f) имеет вид m b. Значение вычисления (m >>= f) имеет тип b. Но поскольку мы не можем вложить ограничение класса в переменную типа b, мы не можем знать, что полученное нами значение удовлетворяет ограничению Ord и поэтому не может использовать это значение как элемент набора, на котором мы хотите иметь возможность вычислять union.

Ответ 2

Недавно на Haskell Cafe Олег привел пример, как эффективно реализовать монаду Set. Цитирование:

... И тем не менее, возможна эффективная подлинная монада Set.

... Прилагается эффективная подлинная монада. Я написал его в прямом стиле (кажется, быстрее, во всяком случае). Ключ состоит в том, чтобы использовать оптимизированную функцию выбора, когда мы можем.

  {-# 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)
  -}

Ответ 3

Я не думаю, что ваши проблемы с производительностью в этом случае связаны с использованием 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 "ограниченной монаде"

Я не уверен, верю ли я ваше утверждение о теореме Гливенко, приводящее к экспоненциальному увеличению (нормализованного) размера доказательства - по крайней мере, в контексте Call-By-Need. Это потому, что мы можем произвольно использовать вторичные доказательства (и наша логика второго порядка, нам нужно только одно доказательство forall a. ~~(a \/ ~a)). Доказательства - это не деревья, они - графики (разделение).

В общем, вы, вероятно, увидите затраты на производительность от Cont wrapping Set, но их обычно можно избежать с помощью

smash :: (Ord r, Ord k) => SetM r r -> SetM k r
smash = fromSet . toSet

Ответ 4

Я узнал еще одну возможность, основанную на расширении GRA 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). Поэтому нельзя использовать комбинаторы типа <*> (или ap) для этой ограниченной монады Set.)