
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/