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

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

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, а не составным. Однако, увеличивая определение (>>=) для 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 вычисляется мгновенно, потому что дублируются только элементарные подвычисления.

Оказывается, что другие решения, включающие 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.

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

... И все же эффективная подлинная монада 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)
  -}

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

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

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

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

Я обнаружил еще одну возможность, основанную на 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 монады.)