[Haskell-cafe] Type famillies & Lifting IO

[Maciej Piechotka]

I started playing with type families. I wanted to achieve, for the
beginning, something like:

> import qualified Control.Monad.IO.Class as IOC
> import Control.Monad.Trans.Class
> import Control.Monad.Trans.Cont
> import Data.Functor.Identity

> class (Monad m, Monad (IO' m)) => MonadIO m where
> type IO' m :: * -> *
> liftIO :: IO a -> IO' m a
> liftM :: m a -> IO' m a

It allows to add IO to computation even if computation originally was
'pure'.

First step was easy:

> instance MonadIO Identity where
> type IO' Identity = IO
> liftIO = id
> liftM = return . runIdentity
> 
> instance MonadIO IO where
> type IO' IO = IO
> liftIO = id
> liftM = id
> 
> instance MonadIO (ST r) where
> type IO' (ST r) = IO
> liftIO = id
> liftM = unsafeSTToIO
> 
> --instance IOC.MonadIO m => MonadIO m where
> --type IO' m = m
> --liftIO = IOC.liftIO
> --liftM = id

However I run into problems - this code doesn't want to compile:

> instance MonadIO m => MonadIO (ContT r m) where
> type IO' (ContT r m) = ContT r (IO' m)
> liftIO f = ContT $ \cont -> liftIO f >>= cont
> liftM f = ContT $ \cont -> liftM f >>= cont

Or this:

> instance MonadIO m => MonadIO (ContT r m) where
> type IO' (ContT r m) = ContT r (IO' m)
> liftIO f = lift . liftIO
> liftM f = lift . liftIO

In fact there is strange interfering types of ghci:

ghci> :t lift . liftIO
lift . liftIO
  :: (m ~ IO' m1, MonadTrans t, Monad m, MonadIO m1) => IO a -> t m a
ghci> :t lift . liftIO :: (m ~ IO' m1, MonadTrans t, Monad m, MonadIO
m1) => IO a -> t m a

:1:7:
Couldn't match expected type `IO' m' against inferred type `m1'
  `m1' is a rigid type variable bound by
   an expression type signature at :1:18
  NB: `IO'' is a type function, and may not be injective
In the second argument of `(.)', namely `liftIO'
In the expression:
lift . liftIO ::
(m ~ (IO' m1), MonadTrans t, Monad m, MonadIO m1) => IO a ->
t m a

What's the problem? I guess I don't understand something basic about
type famillies.

Regards


signature.asc
Description: This is a digitally signed message part
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Type famillies & Lifting IO

[oleg]

Maciej Piechotka wrote:
> class (Monad m, Monad (IO' m)) => MonadIO m where
> type IO' m :: * -> *
> liftIO :: IO a -> IO' m a
> liftM :: m a -> IO' m a

The signature for liftIO betrays a problem. Since liftIO is a member
of a type class, when liftIO is used in code, the type checker has to
find the appropriate instance (i.e., resolve the overloading). Suppose
we have this piece of code:

tt :: FooIO ()
tt = liftIO (return () :: IO ())

How to find the appropriate instance of MonadIO and resolve the liftIO
overloading? The argument type of liftIO does not mention the type
class parameter m at all, and so it is of no guidance for overloading
resolution. We know that the return type of liftIO in the tt code is
FooIO (). Thus we have to find such instance of the MonadIO class that
its associated type IO' m is equal to FooIO. In other words, we have
to find m as a solution of the equation
IO' m = FooIO
Or, we have to invert the type function IO' m. Alas, type functions
are not generally injective and hence not invertible. Indeed, nothing
prevents the user from defining two instances of MonadIO, for types m1
and m2, such that IO' m1 = IO' m2 = FooIO.

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe