Construire des instances de monad efficaces sur `Set` (et d'autres conteneurs avec des contraintes) en utilisant la monade de continuation

Question

Set, de manière similaire à [] a des opérations monadiques parfaitement définies. Le problème est qu'ils nécessitent que les valeurs satisfassent Ord contrainte, et il est donc impossible de définir return et >>= sans aucune contrainte. Le même problème s'applique à de nombreuses autres structures de données qui nécessitent un certain type de contraintes sur les valeurs possibles.

L'astuce standard (suggéré dans un haskell-cafe post) est d'envelopper Set dans la monade de continuation. ContT ne se soucie pas si le foncteur de type sous-jacent a des contraintes. Les contraintes ne deviennent nécessaires lorsque l'emballage/dépliage Set s dans/de continuations:

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 

Cela fonctionne au besoin. Par exemple, nous pouvons simuler une fonction non-déterministe qui soit augmente son argument par 1 ou laisse intact:

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) 

En effet, stepN 5 0 cède fromList [0,1,2,3,4,5]. Si nous avons utilisé [] monade à la place, nous aurions

[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] 

à la place.

---

Le problème est l'efficacité . Si nous appelons stepN 20 0 la sortie prend quelques secondes et stepN 30 0 ne se termine pas dans un délai raisonnable. Il s'avère que toutes les opérations Set.union sont effectuées à la fin, au lieu de les effectuer après chaque calcul monadique. Le résultat est que Set s sont exponentiellement construits et union seulement à la fin, ce qui est inacceptable pour la plupart des tâches.

Y a-t-il un moyen de contourner le problème pour rendre cette construction efficace? J'ai essayé mais sans succès.

(je soupçonne même qu'il pourrait y avoir certains types de limites théoriques suivantes de isomorphisme de Curry-Howard et Glivenko's theorem. Théorème de Glivenko dit que pour toute tautologie propositionnelle φ la formule ¬¬φ peut être prouvée dans la logique intuitionniste Cependant, je soupçonne que la longueur de la preuve (sous sa forme normale) peut être exponentiellement longue, alors, peut-être, il pourrait y avoir des cas où enrouler un calcul dans la continuation monad le rendra exponentiellement plus long?)

Answer 1

Monades sont d'une façon particulière de calculs de structuration et de séquençage. La liaison d'une monade ne peut pas restructurer magiquement votre calcul de manière à se produire de manière plus efficace. Il y a deux problèmes avec la façon dont vous structurez votre calcul.

1. Lors de l'évaluation stepN 20 0, le résultat de step 0 sera calculée 20 fois. C'est parce que chaque étape du calcul produit 0 comme une alternative, qui est ensuite alimenté à l'étape suivante, qui produit également 0 comme alternative, et ainsi de suite ...

   Peut-être un peu de mémoisation ici peut aider.

2. Un problème beaucoup plus important est l'effet de ContT sur la structure de votre calcul. Avec un peu de raisonnement équationnel, élargissant le résultat de replicate 20 step, la définition de foldrM et de simplifier autant de fois que nécessaire, nous pouvons voir que stepN 20 0 équivaut à:

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

   Tous les parenthèses de cette associé d'expression à la la gauche. C'est génial, car cela signifie que le RHS de chaque occurrence de (>>=) est un calcul élémentaire, à savoir step, plutôt qu'un composé. Cependant, un zoom sur la définition de (>>=) pour ContT,

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

   on voit que lors de l'évaluation d'une chaîne de (>>=) associant à gauche, chaque bind poussera un nouveau calcul sur la poursuite en cours c. Pour illustrer ce qui se passe, nous pouvons utiliser à nouveau un peu de raisonnement équationnel, élargir cette définition pour (>>=) et la définition de runContT, et en simplifiant, ce qui donne:

   setReturn 0 `setBind` 
       (\x1 -> step x1 `setBind` 
        (\x2 -> step x2 `setBind` (\x3 -> ...)...) 
   

   Maintenant, pour chaque occurrence de setBind, nous allons demandez-vous quel est l'argument RHS. Pour l'occurrence la plus à gauche, l'argument RHS est l'ensemble du reste du calcul après setReturn 0. Pour la deuxième occurrence, il est tout ce qui suit step x1, etc. Nous allons effectuer un zoom avant la définition de setBind:

   setBind set f = foldl' (\s -> union s . f) empty set 
   

   Ici f représente tout le reste du calcul, tout sur le côté droit d'un événement de setBind. Cela signifie qu'à chaque étape, nous capturons le reste du calcul sous la forme f et que nous appliquons f autant de fois qu'il y a d'éléments dans set. Les calculs ne sont pas élémentaires comme avant, mais plutôt composés, et ces calculs seront dupliqués plusieurs fois.

Le nœud du problème est que le transformateur de monade ContT transforme la structure initiale du calcul, que vous vouliez dire comme une chaîne associative gauche de setBind « s, dans un calcul avec une structure différente, à savoir une chaîne associative droite.C'est après tout parfaitement bien, parce que l'une des lois monade dit que, pour chaque m, f et g nous avons

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

Cependant, les lois monade n'imposent pas que la complexité restent les mêmes de chaque côté les équations de chaque loi. Et en effet, dans ce cas, la manière associative gauche de structurer ce calcul est beaucoup plus efficace. La chaîne associative gauche de setBind évalue en un rien de temps, car seuls les sous-programmes élémentaires sont dupliqués.

Il s'avère que d'autres solutions qui utilisent le Set dans une monade souffrent également du même problème. En particulier, le package set-monad donne des temps d'exécution similaires. La raison en est que, elle aussi, réécrit les expressions associatives de gauche dans les expressions associatives de droite.

Je pense que vous avez mis le doigt sur un problème très important encore assez subtile avec insistant sur le fait que Set une interface obéisse Monad. Et je ne pense pas que cela puisse être résolu. Le problème est que le type de la liaison d'une monade doit être

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

-à-dire aucune contrainte de classe a permis de chaque a ou b. Cela signifie que nous ne pouvons pas imbriquer des liens sur la gauche, sans invoquer d'abord les lois de la monade pour réécrire dans une chaîne associative droite. Voici pourquoi: donné (m >>= f) >>= g, le type de calcul (m >>= f) est de la forme m b. Une valeur du calcul (m >>= f) est de type b. Mais comme nous ne pouvons pas accrocher de contrainte de classe sur la variable de type b, nous ne pouvons pas savoir que la valeur obtenue satisfait une contrainte Ord, et ne peut donc pas utiliser cette valeur comme élément d'un ensemble sur lequel nous voulons pouvoir pour calculer union.

Answer 2

ne pense pas que vos problèmes de performance dans ce cas sont dus à l'utilisation de 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') 

obtient des performances similaires à la mise en œuvre en fonction Cont mais se produit entièrement dans le Set « monade restreint »

Je ne sais pas si je crois que votre demande sur le théorème de Glivenko conduisant à une augmentation exponentielle (normalisée) taille preuve Au moins dans le contexte de l'appel par le besoin. C'est parce que nous pouvons réutiliser arbitrairement subproofs (et notre logique est de deuxième ordre, nous avons besoin d'une seule preuve de forall a. ~~(a \/ ~a)). Les preuves ne sont pas des arbres, ce sont des graphes (partage).

En général, vous êtes susceptibles de voir les coûts de performance de Cont emballage Set mais ils peuvent généralement être évités par

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

Answer 3

Récemment sur Haskell Cafe Oleg gave an example comment implémenter la monade Set efficacement. Citant:

... Et pourtant, le monad Set Set efficace est possible.

... Ci-joint est la véritable monad Set. Je l'ai écrit en style direct (il semble que ce soit plus rapide, de toute façon). La clé est d'utiliser la fonction de sélection optimisée lorsque nous le pouvons.

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

Answer 4

j'ai découvert une autre possibilité, basée sur l'extension ConstraintKinds de GHC. L'idée est de redéfinir Monad pour y inclure une contrainte paramétrique sur les valeurs admises:

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

(Le problème avec cette approche est dans le cas des valeurs monadiques sont des fonctions, telles que m (a -> b), parce qu'ils ne peuvent pas satisfaire contraintes comme Ord (a -> b). donc, on ne peut pas utiliser combinators comme <*> (ou ap) pour cette contrainte Set monade.)