> Ocaml community (where most people strongly rely on type inference
> and do not put types very often)

Well it's the same for Haskell.

> foo :: bar -> foobar -> barfoo
> foo b = let fooAux :: foobar -> barfoo  -- You can comment it out
>            fooAux fb = if f b fb
>                        then fooAux (g b fb)
>                        else h b fb
>        in fooAux

Yes, I also like to write it that way, except you can remove fooAux type signature, and let GHC type inferer do its job, like in OCaml.
Plus, 'foo' signature is merely documentation for you in that case.

> 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.

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.
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.


...Or, remove/comment the inner type signatures ;)


2012/1/4 AUGER Cédric <sedrikov@gmail.com>
Le Tue, 3 Jan 2012 20:46:15 +0100,
Yves Parès <limestrael@gmail.com> 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 <yczhang89@gmail.com>
>
> > On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson
> > <spam@scientician.net> 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
> >