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

Question

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?

Answer 1

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)

Answer 2

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 .

Answer 3

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

Answer 4

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