Costruire istanze monade efficienti su `Set` (e altri contenitori con vincoli) usando il monad di continuazione

Question

Set, analogamente a [] ha una operazione monadica perfettamente definita. Il problema è che richiedono che i valori soddisfino il vincolo Ord e quindi è impossibile definire return e >>= senza alcun vincolo. Lo stesso problema si applica a molte altre strutture di dati che richiedono alcuni tipi di vincoli sui valori possibili.

Il trucco standard (suggeritomi in un haskell-cafe post) è quello di avvolgere Set nella monade di continuazione. ContT non si preoccupa se il functor di tipo sottostante ha vincoli. I vincoli diventano necessarie solo quando la confezione/scartare Set s in/da continuazioni:

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 

Questo funziona in base alle esigenze. Per esempio, possiamo simulare una funzione non deterministica che o aumenta la sua tesi di 1 o lascia intatto:

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) 

Infatti, stepN 5 0 cede fromList [0,1,2,3,4,5]. Se abbiamo usato [] monade, invece, otterremmo

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

invece.

---

Il problema è efficienza. Se chiamiamo stepN 20 0 l'output richiede alcuni secondi e stepN 30 0 non termina entro un ragionevole lasso di tempo. Si scopre che tutte le operazioni Set.union vengono eseguite alla fine, invece di eseguirle dopo ogni calcolo monadico. Il risultato è che in modo esponenziale vengono costruiti molti Set e union solo alla fine, il che è inaccettabile per la maggior parte delle attività.

Esiste un modo per aggirare questa struttura? Ho provato ma senza successo.

(ho anche il sospetto che ci potrebbero essere alcuni tipi di limiti teorici seguito da Curry-Howard isomorfismo e Glivenko's theorem. Il teorema di Glivenko dice che per ogni tautologia proposizionale φ la formula ¬¬φ può essere provato in logica intuizionista . Tuttavia, ho il sospetto che la lunghezza della prova (in forma normale) può essere esponenzialmente lungo. Così, forse, ci potrebbero essere casi in cui avvolgere un calcolo nella monade prosecuzione renderà esponenzialmente più?)

Answer 1

Monadi sono un modo particolare di strutturazione e di sequenziamento calcoli. Il legame di una monade non può ristrutturare magicamente il tuo calcolo in modo tale che avvenga in modo più efficiente. Ci sono due problemi nel modo in cui strutturi il tuo calcolo.

1. Nel valutare stepN 20 0, il risultato di step 0 sarà calcolato 20 volte. Questo perché ogni passo del calcolo produce 0 come un'alternativa, che viene quindi inviata al passaggio successivo, che produce anche 0 come alternativa, e così via ...

   Forse un po 'di memoizzazione qui può aiutare.

2. Un problema molto più grande è l'effetto di ContT sulla struttura del calcolo. Con un po 'di ragionamento equazionale, ampliando il risultato della replicate 20 step, la definizione di foldrM e semplificando, come tante volte quanto necessario, possiamo vedere che stepN 20 0 è equivalente a:

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

   tutte le parentesi di questa espressione associare al sinistra. È grandioso, perché significa che l'RHS di ogni occorrenza di (>>=) è un calcolo elementare, ovvero step, anziché composto. Tuttavia, lo zoom sulla definizione di (>>=) per ContT,

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

   vediamo che quando la valutazione di una catena di (>>=) associare a fianco, ogni bind spingerà un nuovo calcolo sulla prosecuzione corrente c. Per illustrare ciò che sta accadendo, possiamo usare di nuovo un po 'di ragionamento equazionale, ampliando questa definizione per (>>=) e la definizione per runContT, e la semplificazione, ottenendo:

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

   Ora, per ogni occorrenza di setBind, andiamo chiediti quale sia l'argomento RHS. Per l'evento più a sinistra, l'argomento RHS è l'intero resto del calcolo dopo setReturn 0. Per la seconda occorrenza, è tutto dopo step x1, ecc Facciamo ingrandite la definizione di setBind:

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

   Qui f rappresenta tutto il resto del calcolo, tutto sul lato destro di un evento di setBind. Ciò significa che in ogni fase, acquisiamo il resto del calcolo come f e applicando f tante volte quante sono gli elementi in set. I calcoli non sono elementari come prima, ma piuttosto composti, e questi calcoli saranno ripetuti molte volte.

Il nocciolo del problema è che il trasformatore Monade ContT sta trasformando la struttura iniziale del calcolo, che si intende come una catena associativa fianco di setBind 's, in un calcolo con una struttura diversa, cioè una giusta catena associativa.Questo è, dopo tutto perfettamente bene, perché una delle leggi monade dice che, per ogni m, f e g abbiamo

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

Tuttavia, le leggi monade non impongono che la complessità rimangono le stesse su ogni lato le equazioni di ogni legge. E in effetti, in questo caso, il modo associativo sinistro di strutturare questo calcolo è molto più efficiente. La catena associativa di sinistra dei valori di setBind viene valutata in pochissimo tempo, poiché solo le subcomputazioni elementari vengono duplicate.

Si scopre che anche altre soluzioni che scandiscono lo Set in una monade soffrono dello stesso problema. In particolare, il pacchetto set-monad produce runtime simili. La ragione è che anch'essa riscrive le espressioni associative di sinistra in quelle associative giuste.

penso che tu abbia messo il dito su un ma molto importante, piuttosto sottile problema con insistendo sul fatto che Set obbedisce un'interfaccia Monad. E non penso che possa essere risolto. Il problema è che il tipo di legatura di una monade deve essere

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

cioè nessun vincolo classe accettati sia a o b. Ciò significa che non possiamo annidare i legami a sinistra, senza prima invocare le leggi della monade per riscrivere in una giusta catena associativa. Ecco perché: dato (m >>= f) >>= g, il tipo di calcolo (m >>= f) ha il formato m b. Un valore del calcolo (m >>= f) è di tipo b. Ma poiché non possiamo appendere alcun vincolo di classe sulla variabile di tipo b, non possiamo sapere che il valore che abbiamo ottenuto soddisfa un vincolo Ord e, pertanto, non può utilizzare questo valore come elemento di un set su cui vogliamo essere in grado calcolare union.

Answer 2

I don I tuoi problemi di prestazioni in questo caso sono dovuti all'uso di 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') 

ottiene prestazioni simili alla implementazione basata Cont ma avviene interamente nel "Monade ristretta" Set

Non sono sicuro se credo il vostro reclamo circa il teorema di Glivenko portando ad aumento esponenziale (normalizzato) dimensioni a prova - almeno nel contesto Call-By-Need. Questo perché possiamo riutilizzare arbitrariamente i subproof (e la nostra logica è di secondo ordine, abbiamo bisogno solo di una singola prova di forall a. ~~(a \/ ~a)). Le prove non sono alberi, sono grafici (condivisione).

In generale, si rischia di vedere i costi di prestazioni da Cont avvolgendo Set ma in genere possono essere evitati tramite

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

Answer 3

Recentemente su Haskell Cafe Oleg gave an example come implementare il monad Set in modo efficiente. Citando:

... E tuttavia, l'efficace monade Set efficace è possibile.

... In allegato è l'efficace monade Set originale. L'ho scritto in stile diretto (sembra essere più veloce, comunque). La chiave è usare la funzione di scelta ottimizzata quando possiamo.

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

ho scoperto un'altra possibilità, sulla base di ConstraintKinds estensione del GHC. L'idea è quella di ridefinire Monad modo che esso includa un vincolo parametrico valori consentiti:

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

(Il problema con questo approccio è nel caso i valori monadici sono funzioni, come m (a -> b), perché non possono soddisfare vincoli come Ord (a -> b). Quindi non si può usare come combinatori <*> (o ap) per questo costretto Set monade.)