tl;dr avance: seq est le seul moyen.
Depuis la mise en œuvre de l' IO n'est pas prescrit par la norme, on peut seulement regarder les implémentations spécifiques. Si l'on regarde de GHC en œuvre, il est disponible à partir de la source (peut-être que certains de derrière-le-scènes traitement spécial de la IO introduit les violations de la monade des lois, mais je ne suis pas au courant d'un tel événement),
-- 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
il est implémenté comme un (stricte) de l'état monade. Ainsi, toute violation de la monade lois IO fait de, est également faite par Control.Monad.State[.Strict].
Regardons la monade lois et de voir ce qui se passe dans 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
Ignorant le newtype wrapper, qui signifie return x >>= f devient \s -> (f x) s. La seule façon de (peut-être) la distinction que d' f x est seq. (Et seq ne peut distinguer si l' f x ≡ 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
ignorant le newtype wrapper de nouveau, k est remplacé par \s -> k s, ce qui est encore seulement se distinguent par seq, et seulement 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
Maintenant, nous avons généralement
case (case e of case e of
pat1 -> ex1) of ≡ pat1 -> case ex1 of
pat2 -> ex2 pat2 -> ex2
par l'équation 3.17.3 déplacements.(a) de la langue de rapport, de sorte que cette loi ne vaut pas seulement modulo seq.
En résumé, IO satisfait la monade lois, sauf pour le fait qu' seq peut distinguer undefined et \s -> undefined s. La même chose vaut pour State[T], Reader[T], (->) a, et toutes les autres monades l'enveloppant d'un type de fonction.
