haskell - metafísica - monadas filosofia
Construir instancias de mónada eficientes en `Set`(y otros contenedores con restricciones) usando la mónada de continuación (4)
Set
, de forma similar a []
tiene operaciones monádicas perfectamente definidas. El problema es que requieren que los valores satisfagan la restricción Ord
, por lo que es imposible definir return
y >>=
sin restricciones. El mismo problema se aplica a muchas otras estructuras de datos que requieren algún tipo de restricciones sobre los posibles valores.
El truco estándar (sugerido en una publicación de haskell-cafe ) es envolver a Set
en la mónada de continuación. ContT
no se preocupa si el functor de tipo subyacente tiene alguna restricción. Las restricciones solo se necesitan cuando se envuelve / desenvuelve Set
s en / desde continuaciones:
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
Esto funciona según sea necesario. Por ejemplo, podemos simular una función no determinista que aumenta su argumento en 1 o lo deja intacto:
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)
De hecho, stepN 5 0
cede de la fromList [0,1,2,3,4,5]
. Si usáramos []
mónada en su lugar, obtendríamos
[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]
en lugar.
El problema es la eficiencia . Si llamamos a stepN 20 0
la salida tarda unos segundos y stepN 30 0
no finaliza dentro de un tiempo razonable. Resulta que todas Set.union
operaciones de Set.union
se realizan al final, en lugar de realizarlas después de cada cálculo monádico. El resultado es que muchos Set
exponencialmente se construyen y se editan solo al final, lo cual es inaceptable para la mayoría de las tareas.
¿Hay alguna forma de evitarlo, para hacer que esta construcción sea eficiente? Lo intenté pero sin éxito.
(Incluso sospecho que podría haber algún tipo de límites teóricos siguiendo el isomorfismo de Curry-Howard y el teorema de Glivenko. El teorema de Glivenko dice que para cualquier tautología proposicional φ la fórmula ¬¬φ puede demostrarse en lógica intuicionista. Sin embargo, sospecho que el la longitud de la prueba (en forma normal) puede ser exponencialmente larga. Entonces, ¿podría haber casos en que envolver un cálculo en la mónada de continuación lo haga exponencialmente más largo?
Descubrí otra posibilidad, basada en la extensión ConstraintKinds de GHC. La idea es redefinir Monad
para que incluya una restricción paramétrica en los valores permitidos:
{-# 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
(El problema con este enfoque es en el caso de que los valores monádicos sean funciones, como m (a -> b)
, porque no pueden satisfacer restricciones como Ord (a -> b)
. Por lo tanto, no se pueden usar combinadores como <*>
(o ap
) para esta mónada Set
restringida)
Las mónadas son una forma particular de estructurar y secuenciar cálculos. El enlace de una mónada no puede reestructurar mágicamente tu computación para que suceda de una manera más eficiente. Hay dos problemas con la forma en que estructura su computación.
Al evaluar
stepN 20 0
, el resultado delstep 0
se calculará 20 veces. Esto se debe a que cada paso del cálculo produce 0 como una alternativa, que luego se alimenta al siguiente paso, que también produce 0 como alternativa, y así sucesivamente ...Tal vez un poco de memoria aquí puede ayudar.
Un problema mucho más grande es el efecto de
ContT
en la estructura de su computación. Con un poco de razonamiento ecuacional, ampliando el resultado dereplicate 20 step
, la definición defoldrM
y simplificando tantas veces como sea necesario, podemos ver questepN 20 0
es equivalente a:(...(return 0 >>= step) >>= step) >>= step) >>= ...)
Todos los paréntesis de esta expresión se asocian a la izquierda. Eso es genial, porque significa que el RHS de cada ocurrencia de
(>>=)
es un cálculo elemental, es decir, unstep
, en lugar de uno compuesto. Sin embargo, acercando la definición de(>>=)
paraContT
,m >>= k = ContT $ /c -> runContT m (/a -> runContT (k a) c)
vemos que al evaluar una cadena de
(>>=)
asociarse a la izquierda, cada enlace empujará un nuevo cálculo sobre la continuación actualc
. Para ilustrar lo que está sucediendo, podemos utilizar de nuevo un poco de razonamiento ecuacional, ampliando esta definición para(>>=)
y la definición derunContT
, y simplificando, produciendo:setReturn 0 `setBind` (/x1 -> step x1 `setBind` (/x2 -> step x2 `setBind` (/x3 -> ...)...)
Ahora, para cada ocurrencia de
setBind
, preguntémonos cuál es el argumento de RHS. Para la ocurrencia más a la izquierda, el argumento RHS es el resto del cálculo después desetReturn 0
. Para la segunda aparición, es todo después delstep x1
, etc.setBind
la definición desetBind
:setBind set f = foldl'' (/s -> union s . f) empty set
Aquí
f
representa todo el resto del cálculo, todo en el lado derecho de una ocurrencia desetBind
. Eso significa que en cada paso, estamos capturando el resto del cálculo comof
, y aplicandof
tantas veces como elementos en elset
. Los cálculos no son elementales como antes, sino más bien compuestos, y estos cálculos se duplicarán muchas veces.
El quid del problema es que el transformador de ContT
está transformando la estructura inicial del cálculo, que significaba como una cadena asociativa izquierda de setBind
, en un cálculo con una estructura diferente, es decir, una cadena asociativa derecha. Después de todo, esto está perfectamente bien, porque una de las leyes de la mónada dice que, por cada m
, f
y g
que tenemos
(m >>= f) >>= g = m >>= (/x -> f x >>= g)
Sin embargo, las leyes de mónadas no imponen que la complejidad permanezca igual en cada lado de las ecuaciones de cada ley. Y de hecho, en este caso, la forma asociativa izquierda de estructurar este cálculo es mucho más eficiente. La cadena asociativa izquierda de setBind
evalúa en un instante, porque solo las subcomputaciones elementales están duplicadas.
Resulta que otras soluciones de Set
calzados en una mónada también sufren del mismo problema. En particular, el paquete set-monad produce tiempos de ejecución similares. La razón es que también reescribe las expresiones asociativas de la izquierda en asociaciones asociativas de la derecha.
Creo que has puesto el dedo en un problema muy importante pero bastante sutil al insistir en que Set
obedece a una interfaz Monad
. Y no creo que pueda ser resuelto. El problema es que el tipo del enlace de una mónada debe ser
(>>=) :: m a -> (a -> m b) -> m b
es decir, no se permite ninguna restricción de clase en a
o b
. Eso significa que no podemos anidar binds a la izquierda, sin antes invocar las leyes de mónada para reescribir en una cadena asociativa derecha. He aquí por qué: dado (m >>= f) >>= g
, el tipo de cálculo (m >>= f)
es de la forma mb
. Un valor del cálculo (m >>= f)
es de tipo b
. Pero como no podemos colgar ninguna restricción de clase en la variable de tipo b
, no podemos saber que el valor que tenemos satisface una restricción Ord
y, por lo tanto, no podemos usar este valor como el elemento de un conjunto en el que queremos poder para calcular la union
.
No creo que sus problemas de rendimiento en este caso se deben al uso 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'')
obtiene un rendimiento similar a la implementación basada en Cont
, pero ocurre completamente en el Set
"mónada restringida"
No estoy seguro de si creo que su afirmación sobre el teorema de Glivenko lleva a un aumento exponencial del tamaño de la prueba (normalizada), al menos en el contexto Call-By-Need. Esto se debe a que podemos reutilizar arbitrariamente subproofs (y nuestra lógica es de segundo orden, solo necesitamos una prueba única de forall a. ~~(a // ~a)
). Las pruebas no son árboles, son gráficos (compartidos).
En general, es probable que vea los costos de rendimiento del Set
envoltura Cont
Set
pero generalmente se pueden evitar a través de
smash :: (Ord r, Ord k) => SetM r r -> SetM k r
smash = fromSet . toSet
Recientemente en Haskell Cafe Oleg dio un ejemplo de cómo implementar la mónada Set
eficiente. Citando:
... Y, sin embargo, la eficiente mónada Set real es posible.
... Adjunto está la eficaz mónada Set auténtica. Lo escribí en estilo directo (parece ser más rápido, de todos modos). La clave es usar la función de elegir optimizada cuando podamos.
{-# 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) -}