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/ |
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). |
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/ |
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. |
Free forum by Nabble | Edit this page |