[Haskell-cafe] Why does Haskell not infer most general type?

[John Meacham]

On Tue, Apr 06, 2010 at 03:56:32PM -0400, Job Vranish wrote:
> Why does haskell not infer the most general type for these functions? Is it
> a limitation of the algorithm? a limitation of the recursive let binding?
> 
> Any insight would be appreciated :)

This is due to when Haskell does generalizing, first, the definitions
are broken up into strongly connected components based on their
dependencies. Then, in dependency order, the components are type checked
then generalized and the result is added to the environment and made
available to further typechecking. Notably the types are set in stone at
this point and should be the most general they can be.

So what is going on here is that your two function f and y depend on
each other so are part of the same binding group and hence typecheckd
together. this causes y's unknown type to be unified with its use in f,
giving it the more specific Int -> Int type, even though it could be
assigned a more general one.

This is what should happen according to the haskell standard, however,
it was pointed out in the typing haskell in haskell paper that this is
more strict than neccessary, we can furuther split up the binding group
based on 'type dependency' as in, if g and h call each other and g has
an explicit signature, then h need not be considered to depend on it as
the explicit type for g can just be added to the envirornment. When
determining binding groups, we can ignore dependencies through explicit
types effecitively. This was proposed as an extension to haskell 98 in
the THIH paper, and is generally considederd a good idea.

What you have here is a more pathological variation on that, while y
doesn't have an explicit signature, it is used with an explicit one in
f, hence one could theoretically subdivide the binding group, typing f
alone, getting its most general type, then typing y, then going back and
verifying y's use in f is valid. It is ceratinly possible to come up
with a specification for an extended type inference algorithm such as
this, but whether it is worth it is another matter.

        John


-- 
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/