haskell - percepcion - monadas leibniz

¿Un simple ejemplo que muestra que IO no satisface las leyes de mónada?

Question

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

Answer 1

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

Answer 2

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.

Answer 3

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.

Answer 4

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.