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.