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

[Yves Parès]

> 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 at gmail.com>

> Le Tue, 3 Jan 2012 20:46:15 +0100,
> Yves Parès <limestrael at 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 at gmail.com>
> >
> > > On Wed, Jan 4, 2012 at 2:48 AM, Bardur Arantsson
> > > <spam at 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 at haskell.org
> > > http://www.haskell.org/mailman/listinfo/haskell-cafe
> > >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120104/74a521fa/attachment.htm>