monadologia monadas metafísica leibniz filosofia discurso haskell complexity-theory monads continuations curry-howard

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.

  1. Al evaluar stepN 20 0 , el resultado del step 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.

  2. 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 de replicate 20 step , la definición de foldrM y simplificando tantas veces como sea necesario, podemos ver que stepN 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, un step , en lugar de uno compuesto. Sin embargo, acercando la definición de (>>=) para ContT ,

    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 actual c . Para ilustrar lo que está sucediendo, podemos utilizar de nuevo un poco de razonamiento ecuacional, ampliando esta definición para (>>=) y la definición de runContT , 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 de setReturn 0 . Para la segunda aparición, es todo después del step x1 , etc. setBind la definición de setBind :

    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 de setBind . Eso significa que en cada paso, estamos capturando el resto del cálculo como f , y aplicando f tantas veces como elementos en el set . 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) -}