Построение эффективных экземпляров монады в `Set` (и других контейнерах с ограничениями) с использованием монады продолжения
Setаналогично [] имеет четко определенные монадические операции. Проблема в том, что они требуют, чтобы значения удовлетворяли Ord ограничение, и поэтому невозможно определить return а также >>= без каких-либо ограничений. Та же проблема относится ко многим другим структурам данных, которые требуют каких-то ограничений на возможные значения.
Стандартный трюк (предложенный мне в посте на haskell-cafe) - завернуть Setв продолжение монада.ContTне волнует, имеет ли функтор базового типа какие-либо ограничения. Ограничения становятся необходимыми только при обертывании / развёртыванииSets в / из продолжений:
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только в конце, что неприемлемо для большинства задач.
Есть ли способ обойти это, чтобы сделать эту конструкцию эффективной? Я пытался, но безуспешно.
(Я даже подозреваю, что могут существовать некоторые теоретические ограничения, вытекающие из изоморфизма Карри-Говарда и теоремы Гливенко. Теорема Гливенко говорит, что для любой тавтологии высказываний формула может быть доказана в интуиционистской логике. Однако я подозреваю, что Длина доказательства (в нормальной форме) может быть экспоненциально большой. Поэтому, возможно, могут быть случаи, когда перенос вычисления в монаду продолжения сделает его экспоненциально длиннее?)
4 ответа
Монады являются одним из конкретных способов структурирования и упорядочения вычислений. Привязка монады не может волшебным образом перестроить ваши вычисления так, чтобы это произошло более эффективным образом. Есть две проблемы с тем, как вы структурируете свои вычисления.
При оценке
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Оценивает в кратчайшие сроки, потому что дублируются только элементарные подвычисления.
Оказывается, что другие решения обувной 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"S.
Недавно на 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) -}
Я не думаю, что ваши проблемы с производительностью в этом случае связаны с использованием 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 упаковка Set но их обычно можно избежать с помощью
smash :: (Ord r, Ord k) => SetM r r -> SetM k r
smash = fromSet . toSet
Я обнаружил еще одну возможность, основанную на расширении ConstraintKinds от GHC. Идея состоит в том, чтобы переопределить 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 монада.)