Many thanks for the explanation. But I thought that GHC always derives the most generic type, why does it fix my 'a' to 'Int' ? I have another question, now that I know how to pass a generic continuation to evalAST I thought that I could use it to evaluate a more complex language: {-# LANGUAGE GADTs, RankNTypes #-} test = evalAST pr (AppA (SymA "reverse") (TxtA "abc")) t1 = eval $ App (Lit reverse) (Lit "jij") pr :: (Show a) => Expr a -> IO () pr = print . eval evalAST :: (forall a. Show a => Expr a -> IO()) -> AST -> IO () evalAST k (IntA i) = k $ Lit i evalAST k (TxtA i) = k $ Lit i evalAST k (AppA f a) = evalASTFun (\ef -> (evalAST (\ea -> k $ App ef ea) a)) f evalASTFun :: (forall a b. Expr (a-> b) -> IO ()) -> AST -> IO () evalASTFun k (SymA "reverse") = k $ Lit reverse evalASTFun k (SymA "+") = k $ Lit (+) -- An untyped expression data AST = IntA Int | TxtA String | SymA String | AppA AST AST -- A typed expression. data Expr a where Lit :: a -> Expr a App :: Expr (a->b) -> Expr a -> Expr b instance Show (a->b) where show f = "function" eval :: Expr a -> a eval (Lit i) = i eval (App f a) = (eval f) (eval a) But, this won't type check: evalAST k (AppA f a) = evalASTFun (\ef -> (evalAST (\ea -> k $ App ef ea) a)) f My understanding is that GHC correctly complains that the Expr a returned by ea is not necessarily the same Expr 'a' that ef needs. Is there any way out? Thanks, titto On 15 July 2010 11:20, Bas van Dijk wrote:

GHC tries to infer the following type for evalAST2:

evalAST2 :: forall a. (Expr a -> IO()) -> AST -> IO ()

However when the type of 'a' has been found in the first alternatives:

evalAST2 k (IntA i) = k $ Lit i

it is fixed to Int. Then the 'a' doesn't match the type (String) found in the other alternative:

evalAST2 k (TxtA i) = k $ Lit i

The reason why evalAST type checks is that the type of 'k' is

k :: forall a. (Show a) => Expr a -> IO ()

So it works not just for one 'a' but for all of them.

The way to correctly generalize evalAST is by telling GHC that 'k' indeed works for all 'a':

{-# LANGUAGE RankNTypes #-}

evalAST2 :: (forall a. Expr a -> IO()) -> AST -> IO ()

Regards,

Bas

On Thu, Jul 15, 2010 at 11:50 AM, Pasqualino "Titto" Assini wrote:

...

Hi,

can anyone please explain why in the following code evalAST compiles while evalAST2 doesn't?:

Is that because the polymorphic function k is specialised in two different ways in evalAST while in evalAST2 it is constrained to be the same function?

{-# LANGUAGE GADTs #-}

test = evalAST (TxtA "abc")

-- This is OK evalAST :: AST -> IO () evalAST (IntA i) = k $ Lit i evalAST (TxtA i) = k $ Lit i

k :: (Show a) => Expr a -> IO () k e  = print $ eval e

-- This is the same thing, only the k function is passed as a parameter. -- But it won't compile. -- I would expect its type to be: -- evalAST2 :: (Expr a -> IO()) -> AST -> IO () -- But is actually: -- evalAST2 :: (Expr Int -> IO ()) -> AST -> IO () evalAST2 k (IntA i) = k $ Lit i -- evalAST2 k (TxtA i) = k $ Lit i

-- The untyped expression data AST = IntA Int | TxtA String

-- A typed expression. data Expr a where Lit  :: a -> Expr a

eval :: Expr a -> a eval (Lit i) = i

Thanks

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

On Thu, Jul 15, 2010 at 01:20:11PM +0100, Pasqualino Titto Assini wrote:

Many thanks for the explanation.

But I thought that GHC always derives the most generic type, why does it fix my 'a' to 'Int' ?

Note that this type evalAST2 :: forall a. (Expr a -> IO()) -> AST -> IO () means that the type a has to be chosen first, i.e. by the *caller* of evalAST2. So evalAST2 is not free to use its argument k at whatever type it wants, it will be given a function of type (Expr T -> IO()) for some type T that it didn't get to choose. Forcing the caller to provide a polymorphic function, so that evalAST2 can choose at what type(s) to use it, is exactly what is expressed by the rank-2 type evalAST2 :: (forall a. Expr a -> IO()) -> AST -> IO () -Brent