Re: [Haskell-cafe] Solved but strange error in type inference

Le Tue, 3 Jan 2012 20:46:15 +0100, Yves Parès a écrit :

...

Actually, my question is why the different type can't be unified with the inferred type?

Because without ScopedTypeVariable, both types got expanded to :

legSome :: *forall nt* t s. LegGram nt t s -> nt -> Either String ([t], s)

subsome :: *forall nt* t s. [RRule nt t s] -> Either String ([t], s)

So you see subsome declare new variables, which *do not *match the *rigid *ones declared by legSome signature, hence the incompatibility.

How ugly! I thought that Haskell didn't allow to mask type variables. Does that mean that I can do: foo :: (a -> a) -> (b -> b) -> a -> a foo bar dummy = let strange :: a -> a strange = dummy in foo (ok, that's dead code, but how misleading it would be!) Is there some way to enforce a typing error here? (I am pretty sure there is some flag to have explicit 'forall's, but I am not sure that it forces you to use 'forall' explicitely.) I come from Coq community (where forall must be explicit) and Ocaml community (where most people strongly rely on type inference and do not put types very often). I didn't try this example on Ocaml.

As we said before, you have three ways to work it out: 1) Use scoped type variables with explicit forall nt on legSome and *no forall *on subsome, so that nt in subsome matches nt declared in legSome. 2) Don't give a type signature for subsome and let GHC find out which is its correct type. 3) Extract subsome so that it becomes a top-level function with a polymorphic type (Recommended).

In fact I first wanted to write directly the method without using auxiliary functions (I changed my mind since, as I redisigned my code and it wasn't possible [or at least natural for me] to put the code directly inlined). In fact I often do nested functions when there are free variables in the function. I particulary hate to have code like that: foo :: bar -> foobar -> barfoo foo b fb = if f b fb then foo b (g b fb) else h b fb as b is in fact invariant in the calls of 'foo'; so I always rewrite this as: foo :: bar -> foobar -> barfoo foo b = let fooAux :: foobar -> barfoo fooAux fb = if f b fb then fooAux (g b fb) else h b fb in fooAux that is more verbose, but I well see what are the recursive parameters, and I have the (probably wrong) feeling that it is better since function calls have less arguments. Here subsome was depending on the free variable "sg", so I had to generalize it to do so even if I won't have benefits in having the ability to use it elsewhere (as it was the only place I wanted to use it). I always prefer to minimize the number of specialized functions, since I hate jumping from parts of code to other parts of code to understand what a function really does.

Now, concerning the error I asked you to deliberately provoke, that's the quickest way I found to know what is the output of the type inferer, and maybe the only simple one. So this error is:

...

Couldn't match expected type `Int' with actual type `[([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0)' In the expression: subsome :: Int GHC tells you the type it infers for subsome: [([Symbols nt t], [s] -> t0)] -> Either [Char] ([t], t0) The nt you see is the one from legSome, those messages show scoped variables. (You'd get something like 'nt1' or 'nt0' if it was another variable, meant to be instanciated to a different type). This accords with your previous error message, which happens to give you more details about where the rigid type variable nt comes from: `nt' is a rigid type variable bound by the type signature for legSome :: LegGram nt t s -> nt -> Either String ([t], s)

HTH.

2012/1/3 Yucheng Zhang

...

On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson wrote:

...

'subsome' to a different type than the one you intended -- and indeed one which can't be unified with the inferred type. (Unless you use ScopedTypeVariables.)

Thanks for the reply.

Actually, my question is why the different type can't be unified with the inferred type? Could you point me some related resources?

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