6

What is the difference between the two:

recompile :: MonadIO m => Bool -> m Bool
recompile :: Bool -> IO Bool
McBear Holden
  • 5,741
  • 7
  • 33
  • 55

1 Answers1

8

The types forall m. MonadIO m => Bool -> m Bool and Bool -> IO Bool are isomorphic:

{-# LANGUAGE RankNTypes #-}
import Control.Monad.IO.Class

from :: (forall m. MonadIO m => Bool -> m Bool) -> (Bool -> IO Bool)
from act = act

to :: (Bool -> IO Bool) -> (forall m. MonadIO m => Bool -> m Bool)
to act = liftIO . act

Not all types involving IO are isomorphic to a version that replaces IO with a constrained m, though.

Generally, one uses MonadIO m instead of m ~ IO when they feel like scattering liftIO through calling code will be annoying or when there are other mtl-style constraints needed on m; and uses m ~ IO instead of MonadIO m when going for simplicity of API (where MonadIO m contributes to complexity and therefore is not desirable) or when dealing with forking or exception handling (where MonadIO m is not possible for the reasons discussed in the linked question).

Daniel Wagner
  • 145,880
  • 9
  • 220
  • 380
  • And an aside: the proof that `from (to act) = act` is easy. The proof that `to (from act)` is quite a bit trickier, and involves using parametricity to essentially observe that all fully-defined values of type `forall m. MonadIO m => Bool -> m Bool` are equal to `liftIO . foo` for some `foo`. (Yes, even `liftIO bar >> liftIO baz`, which is equal to `liftIO (bar >> baz)` by the `MonadIO` laws.) – Daniel Wagner Sep 18 '18 at 14:13