> Ocaml community (where most people strongly rely on type inference<br>> and do not put types very often)<br><br>Well it's the same for Haskell.<br><br>
> foo :: bar -> foobar -> barfoo<br>
> foo b = let <b>fooAux :: foobar -> barfoo</b> -- You can comment it out<br>
> fooAux fb = if f b fb<br>
> then fooAux (g b fb)<br>
> else h b fb<br>
> in fooAux<br><br>Yes, I also like to write it that way, except you can <b>remove </b>fooAux type signature, and let GHC type inferer do its job, like in OCaml.<br>Plus, 'foo' signature is merely documentation for you in that case.<br>
<br>> I always prefer to minimize the number of specialized functions, since<br>
> I hate jumping from parts of code to other parts of code to understand<br>> what a function really does.<br><br>Too bad, that's one of the assets of functional programming. The more splitted you design your functions, the easier it is to reuse and test them afterwards. A good practice in C-like languages also, IMHO.<br>
You can just write subsome right under legSome, it doesn't break legibility, and if you think it's best tell your module to export only legSome.<br><br><br>...Or, remove/comment the inner type signatures ;)<br><br>
<br><div class="gmail_quote">2012/1/4 AUGER Cédric <span dir="ltr"><<a href="mailto:sedrikov@gmail.com">sedrikov@gmail.com</a>></span><br><blockquote class="gmail_quote" style="margin:0pt 0pt 0pt 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Le Tue, 3 Jan 2012 20:46:15 +0100,<br>
Yves Parès <<a href="mailto:limestrael@gmail.com">limestrael@gmail.com</a>> a écrit :<br>
<div class="im"><br>
> > Actually, my question is why the different type can't be unified<br>
> > with the<br>
> inferred type?<br>
><br>
> Because without ScopedTypeVariable, both types got expanded to :<br>
><br>
</div>> legSome :: *forall nt* t s. LegGram nt t s -> nt -> Either String<br>
> ([t], s)<br>
><br>
> subsome :: *forall nt* t s. [RRule nt t s] -> Either String ([t], s)<br>
><br>
> So you see subsome declare new variables, which *do not *match the<br>
> *rigid *ones declared by legSome signature, hence the incompatibility.<br>
><br>
<br>
How ugly! I thought that Haskell didn't allow to mask type variables.<br>
<br>
Does that mean that I can do:<br>
<br>
foo :: (a -> a) -> (b -> b) -> a -> a<br>
foo bar dummy =<br>
let strange :: a -> a<br>
strange = dummy<br>
in<br>
foo<br>
<br>
(ok, that's dead code, but how misleading it would be!)<br>
<br>
Is there some way to enforce a typing error here?<br>
(I am pretty sure there is some flag to have explicit 'forall's,<br>
but I am not sure that it forces you to use 'forall' explicitely.)<br>
<br>
I come from Coq community (where forall must be explicit) and Ocaml<br>
community (where most people strongly rely on type inference and do not<br>
put types very often). I didn't try this example on Ocaml.<br>
<div class="im"><br>
> As we said before, you have three ways to work it out:<br>
> 1) Use scoped type variables with explicit forall nt on legSome and<br>
</div>> *no forall *on subsome, so that nt in subsome matches nt declared in<br>
<div class="im">> legSome. 2) Don't give a type signature for subsome and let GHC find<br>
> out which is its correct type.<br>
> 3) Extract subsome so that it becomes a top-level function with a<br>
> polymorphic type (Recommended).<br>
<br>
</div>In fact I first wanted to write directly the method without using<br>
auxiliary functions (I changed my mind since, as I redisigned my code<br>
and it wasn't possible [or at least natural for me] to put the code<br>
directly inlined).<br>
<br>
In fact I often do nested functions when there are free variables in<br>
the function. I particulary hate to have code like that:<br>
<br>
foo :: bar -> foobar -> barfoo<br>
foo b fb = if f b fb<br>
then foo b (g b fb)<br>
else h b fb<br>
<br>
as b is in fact invariant in the calls of 'foo'; so I always rewrite<br>
this as:<br>
<br>
foo :: bar -> foobar -> barfoo<br>
foo b = let fooAux :: foobar -> barfoo<br>
fooAux fb = if f b fb<br>
then fooAux (g b fb)<br>
else h b fb<br>
in fooAux<br>
<br>
that is more verbose, but I well see what are the recursive parameters,<br>
and I have the (probably wrong) feeling that it is better since<br>
function calls have less arguments.<br>
<br>
Here subsome was depending on the free variable "sg", so I had to<br>
generalize it to do so even if I won't have benefits in having the<br>
ability to use it elsewhere (as it was the only place I wanted to use<br>
it).<br>
<br>
I always prefer to minimize the number of specialized functions, since<br>
I hate jumping from parts of code to other parts of code to understand<br>
what a function really does.<br>
<div class="HOEnZb"><div class="h5"><br>
><br>
><br>
> Now, concerning the error I asked you to deliberately provoke, that's<br>
> the quickest way I found to know what is the output of the type<br>
> inferer, and maybe the only simple one.<br>
> So this error is:<br>
> > Couldn't match expected type `Int'<br>
> > with actual type `[([Symbols nt t], [s] -> t0)]<br>
> > -> Either [Char] ([t], t0)'<br>
> > In the expression: subsome :: Int<br>
> GHC tells you the type it infers for subsome: [([Symbols nt t], [s]<br>
> -> t0)] -> Either [Char] ([t], t0)<br>
> The nt you see is the one from legSome, those messages show scoped<br>
> variables. (You'd get something like 'nt1' or 'nt0' if it was another<br>
> variable, meant to be instanciated to a different type).<br>
> This accords with your previous error message, which happens to give<br>
> you more details about where the rigid type variable nt comes from:<br>
> > `nt' is a rigid type variable bound by<br>
> > the type signature for<br>
> > legSome :: LegGram nt t s -> nt -> Either String ([t],<br>
> > s)<br>
><br>
> HTH.<br>
><br>
> 2012/1/3 Yucheng Zhang <<a href="mailto:yczhang89@gmail.com">yczhang89@gmail.com</a>><br>
><br>
> > On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson<br>
> > <<a href="mailto:spam@scientician.net">spam@scientician.net</a>> wrote:<br>
> > > 'subsome' to a different type than the one you intended -- and<br>
> > > indeed one which can't be unified with the inferred type. (Unless<br>
> > > you use ScopedTypeVariables.)<br>
> ><br>
> > Thanks for the reply.<br>
> ><br>
> > Actually, my question is why the different type can't be unified<br>
> > with the inferred type? Could you point me some related resources?<br>
> ><br>
> > _______________________________________________<br>
> > Haskell-Cafe mailing list<br>
> > <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
> > <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
> ><br>
<br>
</div></div></blockquote></div><br>