haskell - percepcion - monadas leibniz
¿Un simple ejemplo que muestra que IO no satisface las leyes de mónada? (4)
Todas las mónadas en Haskell son solo mónadas si excluyes el raro combinador de seq
. Esto también es cierto para IO
. Como seq
no es realmente una función normal, sino que implica magia, debe excluirla de la comprobación de las leyes de mónada por la misma razón por la que debe excluir la forma de unsafePerformIO
. Usando seq
puedes probar que todas las mónadas están equivocadas, de la siguiente manera.
En la categoría de Kleisli, la mónada da lugar a, el return
es el morfismo de identidad y (<=<)
es la composición. Entonces el return
debe ser una identidad para (<=<)
:
return <=< x = x
Usando seq
even Identity y Maybe no pueden ser mónadas:
seq (return <=< undefined :: a -> Identity b) () = ()
seq (undefined :: a -> Identity b) () = undefined
seq (return <=< undefined :: a -> Maybe b) () = ()
seq (undefined :: a -> Maybe b) () = undefined
He visto mencionar que IO
no satisface las leyes de mónadas, pero no encontré un ejemplo simple que lo muestre. Alguien sabe un ejemplo? Gracias.
Editar: Como ertes y nm, usar seq
es un poco ilegal ya que puede hacer que cualquier mónada falle las leyes (combinadas con undefined
). Como undefined
puede verse como un cálculo sin terminación, está perfectamente bien usarlo.
Entonces la pregunta revisada es: ¿Alguien sabe un ejemplo que muestra que IO
no cumple con las leyes de mónadas, sin usar seq
? (¿O tal vez una prueba de que IO
cumple con las leyes si seq
no está permitido?)
Una de las leyes de la mónada es que
m >>= return ≡ m
Probémoslo en GHCi:
Prelude> seq ( undefined >>= return :: IO () ) "hello, world"
"hello, world"
Prelude> seq ( undefined :: IO () ) "hello, world"
*** Exception: Prelude.undefined
Tan undefined >>= return
no es lo mismo que undefined
, por lo tanto IO
no es una mónada. Si intentamos lo mismo para Maybe
Monada, por otro lado:
Prelude> seq ( undefined >>= return :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined
Prelude> seq ( undefined :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined
Las dos expresiones son idénticas, por lo tanto, este ejemplo no excluye que Maybe
sea una mónada.
Si alguien tiene un ejemplo que no se base en el uso de seq
o undefined
, estaría interesado en verlo.
tl; dr por adelantado: seq
es la única manera.
Dado que la implementación de IO
no está prescrita por el estándar, solo podemos observar implementaciones específicas. Si miramos la implementación de GHC, ya que está disponible desde la fuente (puede ser que parte del tratamiento especial detrás de escena de IO
introduzca violaciones de las leyes de mónadas, pero no estoy al tanto de tal suceso),
-- in GHC.Types (ghc-prim)
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
-- in GHC.Base (base)
instance Monad IO where
{-# INLINE return #-}
{-# INLINE (>>) #-}
{-# INLINE (>>=) #-}
m >> k = m >>= / _ -> k
return = returnIO
(>>=) = bindIO
fail s = failIO s
returnIO :: a -> IO a
returnIO x = IO $ / s -> (# s, x #)
bindIO :: IO a -> (a -> IO b) -> IO b
bindIO (IO m) k = IO $ / s -> case m s of (# new_s, a #) -> unIO (k a) new_s
thenIO :: IO a -> IO b -> IO b
thenIO (IO m) k = IO $ / s -> case m s of (# new_s, _ #) -> unIO k new_s
unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
unIO (IO a) = a
se implementa como una mónada de estado (estricta). Por lo tanto, cualquier violación de las leyes de mónada que IO
haga, también es hecha por Control.Monad.State[.Strict]
.
Miremos las leyes de la mónada y veamos qué sucede en IO
:
return x >>= f ≡ f x:
return x >>= f = IO $ /s -> case (/t -> (# t, x #)) s of
(# new_s, a #) -> unIO (f a) new_s
= IO $ /s -> case (# s, x #) of
(# new_s, a #) -> unIO (f a) new_s
= IO $ /s -> unIO (f x) s
Ignorando el envoltorio de tipo nuevo, eso significa que el return x >>= f
convierte en /s -> (fx) s
. La única forma de (posiblemente) distinguir eso de fx
es seq
. (Y seq
solo puede distinguirlo si fx ≡ undefined
.)
m >>= return ≡ m:
(IO k) >>= return = IO $ /s -> case k s of
(# new_s, a #) -> unIO (return a) new_s
= IO $ /s -> case k s of
(# new_s, a #) -> (/t -> (# t, a #)) new_s
= IO $ /s -> case k s of
(# new_s, a #) -> (# new_s, a #)
= IO $ /s -> k s
haciendo caso omiso de la nueva envoltura de tipo nuevo, k
se reemplaza por /s -> ks
, que de nuevo solo se distingue por seq
, y solo si k ≡ undefined
.
m >>= (/x -> g x >>= h) ≡ (m >>= g) >>= h:
(IO k) >>= (/x -> g x >>= h) = IO $ /s -> case k s of
(# new_s, a #) -> unIO ((/x -> g x >>= h) a) new_s
= IO $ /s -> case k s of
(# new_s, a #) -> unIO (g a >>= h) new_s
= IO $ /s -> case k s of
(# new_s, a #) -> (/t -> case unIO (g a) t of
(# new_t, b #) -> unIO (h b) new_t) new_s
= IO $ /s -> case k s of
(# new_s, a #) -> case unIO (g a) new_s of
(# new_t, b #) -> unIO (h b) new_t
((IO k) >>= g) >>= h = IO $ /s -> case (/t -> case k t of
(# new_s, a #) -> unIO (g a) new_s) s of
(# new_t, b #) -> unIO (h b) new_t
= IO $ /s -> case (case k s of
(# new_s, a #) -> unIO (g a) new_s) of
(# new_t, b #) -> unIO (h b) new_t
Ahora, generalmente tenemos
case (case e of case e of
pat1 -> ex1) of ≡ pat1 -> case ex1 of
pat2 -> ex2 pat2 -> ex2
según la ecuación 3.17.3.(a) del informe de idioma, por lo que esta ley no solo contiene el módulo seq
.
Resumiendo, IO
satisface las leyes de la mónada, excepto por el hecho de que seq
puede distinguir undefined
y /s -> undefined s
. Lo mismo vale para el State[T]
, el Reader[T]
, (->) a
y cualquier otra mónada que envuelva un tipo de función.
m >>= return ≡ m
está roto:
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: IO ()
agolpa la memoria y aumenta el tiempo de cálculo, mientras
sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: Maybe ()
no.
AFAIR hay un Transformador Monad que resuelve este problema; si adivino bien, es el Codensity Monad Transformer.