CODEWITHSUNDEEP
haskelltypes
Blezz
Blezz

Reputation: 323

Haskell: function signature

This program compiles without problems:

bar :: MonadIO m
    => m String
bar = undefined

run2IO :: MonadIO m
       => m String
       -> m String
run2IO foo  = liftIO bar

When I change bar to foo (argument name),

run2IO :: MonadIO m
       => m String
       -> m String
run2IO foo  = liftIO foo

I get:

Couldn't match type ‘m’ with ‘IO’ ‘m’ is a rigid type variable bound by the type signature for run2IO :: MonadIO m => m String -> m String ...

Expected type: IO String Actual type: m String ...

Why are the 2 cases are not equivalent?

Upvotes: 3

Views: 743

Answers (2)

Alexis King
Alexis King

Reputation: 43842

Remember the type of liftIO:

liftIO :: MonadIO m => IO a -> m a

Importantly, the first argument must be a concrete IO value. That means when you have an expression liftIO x, then x must be of type IO a.

When a Haskell function is universally quantified (using an implicit or explicit forall), then that means the function caller chooses what the type variable is replaced by. As an example, consider the id function: it has type a -> a, but when you evaluate the expression id True, then id takes the type Bool -> Bool because a is instantiated as the Bool type.

Now, consider your first example again:

run2IO :: MonadIO m => m Integer -> m Integer
run2IO foo = liftIO bar

The foo argument is completely irrelevant here, so all that actually matters is the liftIO bar expression. Since liftIO requires its first argument to be of type IO a, then bar must be of type IO a. However, bar is polymorphic: it actually has type MonadIO m => m Integer.

Fortunately, IO has a MonadIO instance, so the bar value is instantiated using IO to become IO Integer, which is okay, because bar is universally quantified, so its instantiation is chosen by its use.

Now, consider the other situation, in which liftIO foo is used, instead. This seems like it’s the same, but it actually isn’t at all: this time, the MonadIO m => m Integer value is an argument to the function, not a separate value. The quantification is over the entire function, not the individual value. To understand this more intuitively, it might be helpful to consider id again, but this time, consider its definition:

id :: a -> a
id x = x

In this case, x cannot be instantiated to be Bool within its definition, since that would mean id could only work on Bool values, which is obviously wrong. Effectively, within the implementation of id, x must be used completely generically—it cannot be instantiated to a specific type because that would violate the parametricity guarantees.

Therefore, in your run2IO function, foo must be used completely generically as an arbitrary MonadIO value, not a specific MonadIO instance. The liftIO call attempts to use the specific IO instance, which is disallowed, since the caller might not provide an IO value.

It is possible, of course, that you might want the argument to the function to be quantified in the same way as bar is; that is, you might want its instantiation to be chosen by the implementation, not the caller. In that case, you can use the RankNTypes language extension to specify a different type using an explicit forall:

{-# LANGUAGE RankNTypes #-}

run3IO :: MonadIO m => (forall m1. MonadIO m1 => m1 Integer) -> m Integer
run3IO foo = liftIO foo

This will typecheck, but it’s not a very useful function.

Upvotes: 9

leftaroundabout
leftaroundabout

Reputation: 120711

In the first, you're using liftIO on bar. That actually requires bar :: IO String. Now, IO happens to be (trivially) an instance on MonadIO, so this works – the compiler simply throws away the polymorphism of bar.

In the second case, the compiler doesn't get to decide what particular monad to use as the type of foo: it's fixed by the environment, i.e. the caller can decide what MonadIO instance it should be. To again get the freedom to choose IO as the monad, you'd need the following signature:

{-# LANGUAGE Rank2Types, UnicodeSyntax #-}

run2IO' :: MonadIO m
       => (∀ m' . MonadIO m' => m' String)
       -> m String
run2IO' foo  = liftIO foo

... however I don't think you really want that: you might then as well write

run2IO' :: MonadIO m => IO String -> m String
run2IO' foo  = liftIO foo

or simply run2IO = liftIO.

Upvotes: 5

Related Questions