Inferred type is less polymorphic than e

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|

Inferred type is less polymorphic than e

Marco Túlio Gontijo e Silva-4
Hello,

I'm getting this error message from GHC in the following code:


> type M a = Monad m => m a

> class A a b where
>   f :: Monad m => a -> m b

> instance A String Char where
>   f string = return $ head string

> instance A Char Int where
>   f int = return $ fromEnum int

I thought at first to write h like this, but it gives me the error.  If
I write it like the other h uncommented, there's no error.  I can't see
why they aren't equivalent.

h :: IO ()
h = f "abc" >>= (f :: Char -> M Int) >>= print

> h :: IO ()
> h = (f "abc" :: M Char) >>= f >>= (print :: Int -> IO ())

Can someone clarify this to me?

Greetings.

--
marcot
http://marcot.iaaeee.org/


Reply | Threaded
Open this post in threaded view
|

Inferred type is less polymorphic than e

Daniel Fischer-4
Am Donnerstag 09 April 2009 00:29:24 schrieb Marco T?lio Gontijo e Silva:

> Hello,
>
> I'm getting this error message from GHC in the following code:
> > type M a = Monad m => m a
> >
> > class A a b where
> >   f :: Monad m => a -> m b
> >
> > instance A String Char where
> >   f string = return $ head string
> >
> > instance A Char Int where
> >   f int = return $ fromEnum int
>
> I thought at first to write h like this, but it gives me the error.  If
> I write it like the other h uncommented, there's no error.  I can't see
> why they aren't equivalent.
>
> h :: IO ()
> h = f "abc" >>= (f :: Char -> M Int) >>= print
>
> > h :: IO ()
> > h = (f "abc" :: M Char) >>= f >>= (print :: Int -> IO ())
>
> Can someone clarify this to me?
>
> Greetings.

The first error message when loading that code is

Inferred.hs:3:0:
    Illegal polymorphic or qualified type:
      forall (m :: * -> *). (Monad m) => m a
    Perhaps you intended to use -XRankNTypes or -XRank2Types
    In the type synonym declaration for `M'                

That can be a hint. The type synonym M is probably not what you think.

This:
----------------------------------------------------------------
class B a b where
    foo :: a -> M b

instance B String Char where
    foo str = return $ head str

instance B Char Int where
    foo c = return $ fromEnum c

k :: IO ()
k = foo "abc" >>= (foo :: Char -> M Int) >>= print
----------------------------------------------------------------

works, as does

m = foo "abc" >>= (foo :: Char -> (forall x. Monad x => x Int)) >>= print

And that reveals what's going on, since m is in fact the same as k.
The type of f in class A says that given any specific monad m and a value of
type a, f can produce a value of type m b.
But when you write
(f :: Char -> M Int)
, you say that given a Char, f produces a value which belongs to m Int *for
every monad m*. Thus the type you state for f (the expected type) is more
polymorphic than the actual type f has according to the class definition (which
is the inferred type).

Reply | Threaded
Open this post in threaded view
|

Inferred type is less polymorphic than e

Marco Túlio Gontijo e Silva-4
Em Qui, 2009-04-09 ?s 01:55 +0200, Daniel Fischer escreveu:

> Am Donnerstag 09 April 2009 00:29:24 schrieb Marco T?lio Gontijo e Silva:
> > Hello,
> >
> > I'm getting this error message from GHC in the following code:
> > > type M a = Monad m => m a
> > >
> > > class A a b where
> > >   f :: Monad m => a -> m b
> > >
> > > instance A String Char where
> > >   f string = return $ head string
> > >
> > > instance A Char Int where
> > >   f int = return $ fromEnum int
> >
> > I thought at first to write h like this, but it gives me the error.  If
> > I write it like the other h uncommented, there's no error.  I can't see
> > why they aren't equivalent.
> >
> > h :: IO ()
> > h = f "abc" >>= (f :: Char -> M Int) >>= print
> >
> > > h :: IO ()
> > > h = (f "abc" :: M Char) >>= f >>= (print :: Int -> IO ())
> >
> ----------------------------------------------------------------
> class B a b where
>     foo :: a -> M b
>
> instance B String Char where
>     foo str = return $ head str
>
> instance B Char Int where
>     foo c = return $ fromEnum c
>
> k :: IO ()
> k = foo "abc" >>= (foo :: Char -> M Int) >>= print
> ----------------------------------------------------------------
>
> works, as does
>
> m = foo "abc" >>= (foo :: Char -> (forall x. Monad x => x Int)) >>= print
>
> And that reveals what's going on, since m is in fact the same as k.
> The type of f in class A says that given any specific monad m and a value of
> type a, f can produce a value of type m b.
> But when you write
> (f :: Char -> M Int)
> , you say that given a Char, f produces a value which belongs to m Int *for
> every monad m*. Thus the type you state for f (the expected type) is more
> polymorphic than the actual type f has according to the class definition (which
> is the inferred type).

Ok, I got it, so I tried changing class A in my example to:

> class A a b where
>   f :: forall m . Monad m => a -> m b

so that the type of f would be as polymorphic as the type a -> M b.  But
I got the same problem.

Your solution is good, but I can't do it in my real application where I
find out this problem, because the type synonym M is defined after the
class A, and it contains more than on type constraint:

> type Interpret value
>   = ( MonadReader Input monad
>     , MonadState Machine monad
>     , MonadWriter Stream monad)
>   => monad value

My use is that I have some classes defined in modules included by the
one that defines type Interpret, like this:

> class Value pointer value where
>   getValue
>     :: (MonadReader Program monad, MonadState Machine monad)
>     => pointer -> monad value

And even if they were defined in the same file, it would not be good to
define them as Interpret, because it would restrict its type.

Another thing:  I understand your explanation, but I don't get why this
makes the other h definition valid.  Could you clarify me on that?

Thanks.

--
marcot
http://marcot.iaaeee.org/


Reply | Threaded
Open this post in threaded view
|

Inferred type is less polymorphic than e

Daniel Fischer-4
Am Donnerstag 09 April 2009 13:16:01 schrieb Marco T?lio Gontijo e Silva:
> Em Qui, 2009-04-09 ?s 01:55 +0200, Daniel Fischer escreveu:
> Ok, I got it, so I tried changing class A in my example to:
> > class A a b where
> >   f :: forall m . Monad m => a -> m b
>
> so that the type of f would be as polymorphic as the type a -> M b.  But
> I got the same problem.

Because that's exactly the same type f had before.
To get a polymorphic result from f, you have to declare

{-# LANGUAGE Rank2Types #-}
-- or make it RankNTypes and be ready for more quantification

class A a b where
    f :: a -> (forall m. Monad m => m b)

>
> Your solution is good, but I can't do it in my real application where I
> find out this problem, because the type synonym M is defined after the
>
> class A, and it contains more than on type constraint:
> > type Interpret value
> >   = ( MonadReader Input monad
> >     , MonadState Machine monad
> >     , MonadWriter Stream monad)
> >   => monad value
>
> My use is that I have some classes defined in modules included by the
>
> one that defines type Interpret, like this:
> > class Value pointer value where
> >   getValue
> >
> >     :: (MonadReader Program monad, MonadState Machine monad)
> >
> >     => pointer -> monad value
>
> And even if they were defined in the same file, it would not be good to
> define them as Interpret, because it would restrict its type.
>
> Another thing:  I understand your explanation, but I don't get why this
> makes the other h definition valid.  Could you clarify me on that?

This definition?
> > > h :: IO ()
> > > h = (f "abc" :: M Char) >>= f >>= (print :: Int -> IO ())

Let's start on the left:

(f "abc" :: M Char) === (f "abc" :: forall m. Monad m => m Char)

Now we have

class A a b where
    f :: Monad m => a -> m b

instance A String Char where ...

We apply f to the String "abc", so an "instance A String b" has to be selected.

f will here be invoked at the type

(A String b, Monad m) => String -> m b
    === forall m b. (A String b, Monad m) => String -> m b

Therefore f "abc" has the type resulting from removing the argument type, namely

f "abc" :: forall m b. (A String b, Monad m) => m b

Note that although f does not have the type
(A String b) => String -> (forall m. Monad m => m b)

the expression (f string) has the type forall b m. (A String b, Monad m) => m b.

It's the same with return, the type of return is
forall a m. Monad m => a -> m a
and not
forall a. a -> (forall m. Monad m => m a),
but the type of return value is (forall m. Monad m => m a), where a is the type of value.

Now f "abc" has a type annotation, f "abc" :: M Char, or
f "abc" :: forall m. Monad m => m Char

That type must now be unified with the inferred type,
forall mon b. (A String b, Monad mon) => mon b.

It is obvious that we must have b === Char, so the compiler looks for an
instance A String Char where... (or a more general instance)

Since there is one, that is fine and the satisfied constraint (A String Char) can be
removed. The two type(-constructor) variables m and mon are now unified and there contexts
united. Since both contexts are the same, the result is

f "abc" :: forall m. Monad m => m Char,
exactly the specified signature (can't be anything else, if the inferred type were less
polymorphic than the specified, it wouldn't compile, if it's more general, it's restricted
to the specified type).

On to the next step, look at

(f "abc" :: M Char) >>= f

(>>=) :: Monad m => m u -> (u -> m v) -> m v
(f "abc") :: Monad mo => mo Char
f :: (A a b, Monad mon) => a -> mon b

Now we have to unify mo Char with m u (the contexts Monad m and Monad mo will be taken
care of thereafter).
That's easy, u == Char and m === mo, contexts are the same, so

((f "abc" :: M Char) >>=) :: Monad m => (Char -> m v) -> m v

Next we must unify
Char -> m v
with
a -> mon b.
That's again easy, a === Char, mon === m, b === v.
Now take the contexts (Monad m) and (A a b, Monad mon) into account.
Substituting int f's context, we get the context (A Char v, Monad m) for f's type here,
so this f is called at the type (A Char v, Monad m) => Char -> m v, and we get the type

(f "abc" :: M Char) >>= f :: (A Char v, Monad m) => m v

Finally,

left :: (A Char v, Monad m) => m v
(>>=) :: Monad mo => mo a -> (a -> mo b) -> mo b
print :: Int -> IO ()         -- specified

We get the type

(left >>=) :: (A Char v, Monad m) => (v -> m b) -> m b

and then must unify (v -> m b) with (Int -> IO ()), giving v === Int, m === IO, b === ().
Substituting into the contexts gives

(left >>= print) :: (A Char Int, Monad IO) => IO ()

The context doesn't contain any type variables and the conditions are fulfilled, so the
context is removed, leaving

(f "abc" :: M Char) >>= f >>= (print :: Int -> IO ()) :: IO ().

>
> Thanks.