Prosty przykład pokazujący, że IO nie spełnia praw monad?

Question

Prosty przykład pokazujący, że IO nie spełnia praw monad?

Widziałem, że IO nie spełnia praw monad, ale nie znalazłem prostego przykładu na to wskazującego. Ktoś zna przykład? Dzięki.

Edit: jak zauważyli ertes i N. M., używanie seq jest trochę nielegalne, ponieważ może sprawić, że każda monada zawiedzie prawa(w połączeniu z undefined). Ponieważ undefined może być postrzegane jako niekończące się obliczenia, można go używać.

Więc zmienione pytanie brzmi: ktoś zna przykład pokazanie, że IO nie spełnia praw monad, bez użycia seq? (A może dowód, że IO spełnia prawa, Jeśli seq nie jest dozwolone?)

38

haskell functional-programming io monads

Author: Community, 2012-09-27

Source

4 answers

Wszystkie monady w Haskell są tylko monadami, jeśli wykluczysz dziwny kombinator seq. Dotyczy to również IO. Ponieważ seq nie jest w rzeczywistości funkcją regularną, ale wiąże się z magią, musisz wykluczyć ją z sprawdzania praw monad z tego samego powodu, dla którego musisz wykluczyć unsafePerformIO. Używając seq możesz udowodnić, że wszystkie monady są błędne, w następujący sposób.

W kategorii Kleisli monada daje początek, return jest morfizmem tożsamościowym, a (<=<) jest kompozycją. Więc return musi być tożsamością dla (<=<):

return <=< x = x

Używając seq nawet tożsamości i może nie być monad:

seq (return <=< undefined :: a -> Identity b) () = ()
seq (undefined            :: a -> Identity b) () = undefined

seq (return <=< undefined :: a -> Maybe b) () = ()
seq (undefined            :: a -> Maybe b) () = undefined

42

Author: ertes,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/doraprojects.net/template/agent.layouts/content.php on line 54
2015-10-12 17:17:49

Jedno z praw monad jest takie, że

m >>= return ≡ m

Spróbujmy w GHCi:

Prelude> seq ( undefined >>= return :: IO () ) "hello, world"
"hello, world"

Prelude> seq ( undefined :: IO () ) "hello, world"
*** Exception: Prelude.undefined

Zatem undefined >>= return nie jest tym samym co undefined, zatem IO nie jest monadą. Jeśli spróbujemy tego samego dla Maybe monady, z drugiej strony:

Prelude> seq ( undefined >>= return :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined

Prelude> seq ( undefined :: Maybe () ) "hello, world"
*** Exception: Prelude.undefined

Oba wyrażenia są identyczne - więc Maybe nie jest wykluczone z bycia monadą przez ten przykład.

Jeśli ktoś ma przykład, który nie opiera się na użyciu seq lub undefined, byłbym zainteresowany, aby go zobaczyć.

8

Author: Chris Taylor,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/doraprojects.net/template/agent.layouts/content.php on line 54
2012-09-27 09:14:25

m >>= return ≡ m

Jest złamane:

sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: IO ()

Zaśmieca pamięć i zwiększa czas obliczeń, podczas gdy

sequence_ $ take 100000 $ iterate (>>=return) (return ()) :: Maybe ()

Nie. Jest transformator Monad, który rozwiązuje ten problem; jeśli dobrze myślę, To jest to transformator Monad Codensity.

4

Author: comonad,
Warning: date(): Invalid date.timezone value 'Europe/Kyiv', we selected the timezone 'UTC' for now. in /var/www/agent_stack/data/www/doraprojects.net/template/agent.layouts/content.php on line 54
2012-10-15 18:00:17

score 25 · Accepted Answer

Tl;dr: seq jest jedynym sposobem.

Ponieważ implementacja IO nie jest określona przez standard, możemy przyjrzeć się tylko konkretnym implementacjom. Jeśli spojrzymy na implementację GHC, ponieważ jest ona dostępna ze źródła (może być tak ,że niektóre specjalne traktowanie za kulisami IO wprowadza naruszenia praw monad, ale nie jestem świadomy takiego zdarzenia),

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

Jest zaimplementowany jako (ścisła) monada stanowa. Więc każde naruszenie monady prawa IO sprawia, jest również przez Control.Monad.State[.Strict].

Spójrzmy na prawa monad i zobaczmy, co się stanie w 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

Ignorowanie wrappera newtype oznacza, że return x >>= f staje się \s -> (f x) s. Jedynym sposobem na (ewentualnie) odróżnienie tego od f x jest seq. (I seq może ją odróżnić tylko wtedy, gdy 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

Ignorując ponownie wrapper newtype, k jest zastępowany przez \s -> k s, który ponownie odróżnia się tylko przez seq i tylko wtedy, gdy 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

Teraz, my ogólnie mają

case (case e of                    case e of
        pat1 -> ex1) of       ≡      pat1 -> case ex1 of
  pat2 -> ex2                                  pat2 -> ex2

Na równanie 3.17.3.a) raportu językowego, więc prawo to posiada nie tylko modulo seq.

Podsumowując, IO spełnia prawa monad, z wyjątkiem tego, że seq potrafi odróżnić undefined i \s -> undefined s. To samo dotyczy State[T], Reader[T], (->) a, oraz wszelkie inne monady zawierające typ funkcji.