Why does Haskell not infer most general type?
Is haskell supposed to always infer the most general type (barring extensions)? I found a simple case where this is not true: f _ = undefined where _ = y :: Int -> Int y x = undefined where _ = f x Haskell infers the types of 'y' and 'f' as: f :: Int -> a y :: Int -> Int This confused me at first, but after thinking about it a while it seemed to make sense. But then my friend John pointed out that you can add type sigs for 'f' and 'y': f :: a -> b y :: a -> b and have it still typecheck! This thoroughly confused me. 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 :) - Job
On Apr 6, 2010, at 15:56 , Job Vranish wrote:
Is haskell supposed to always infer the most general type (barring extensions)?
Look up the monomorphism restriction. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
I don't believe that the monomorphism restriction has anything to do with this. Removing it does not generalize the type. On Tue, Apr 6, 2010 at 4:46 PM, Brandon S. Allbery KF8NH < allbery@ece.cmu.edu> wrote:
On Apr 6, 2010, at 15:56 , Job Vranish wrote:
Is haskell supposed to always infer the most general type (barring extensions)?
Look up the monomorphism restriction.
-- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Excerpts from Brandon S. Allbery KF8NH's message of Tue Apr 06 16:46:28 -0400 2010:
On Apr 6, 2010, at 15:56 , Job Vranish wrote:
Is haskell supposed to always infer the most general type (barring extensions)? Look up the monomorphism restriction.
Hey Brandon, I tested the code with -XNoMonomorphismRestriction and it still inferred the specific type, so perhaps this is either a GHC bug or something different? wnoise also points out that both functions take arguments, so the monomorphism restriction doesn't apply. See: http://www.reddit.com/r/haskell/comments/bn9to/type_checker_trivia_what_are_... Cheers, Edward
On Tue, Apr 06, 2010 at 03:56:32PM -0400, Job Vranish wrote:
f _ = undefined where _ = y :: Int -> Int
y x = undefined where _ = f x
Because f and y are mutually recursive, their types are inferred together, so y gets the type Int -> Int (as given), which forces f :: Int -> a. If you add the type signature f :: a -> b, you break the cycle: that type is used in inferring the type of y (namely a -> b), which is then used in checking the typeof f. Ditto if you add y :: a -> b instead. (This is not Haskell 98, but the implementations have done this for years, and it will be in Haskell 2010.)
So in Haskell 98, would the added constraints result in a type error?
- Job
On Tue, Apr 6, 2010 at 5:12 PM, Ross Paterson
On Tue, Apr 06, 2010 at 03:56:32PM -0400, Job Vranish wrote:
f _ = undefined where _ = y :: Int -> Int
y x = undefined where _ = f x
Because f and y are mutually recursive, their types are inferred together, so y gets the type Int -> Int (as given), which forces f :: Int -> a.
If you add the type signature f :: a -> b, you break the cycle: that type is used in inferring the type of y (namely a -> b), which is then used in checking the typeof f. Ditto if you add y :: a -> b instead. (This is not Haskell 98, but the implementations have done this for years, and it will be in Haskell 2010.) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Tue, Apr 06, 2010 at 05:18:34PM -0400, Job Vranish wrote:
So in Haskell 98, would the added constraints result in a type error?
Yes, because the types of the mutually recursive identifiers would be inferred together without using the type signatures, and then would fail to match the declared types. But then there aren't any implementations of Haskell 98 to test this on.
Thank you all for your replies. This is all much more clear now :)
- Job
On Tue, Apr 6, 2010 at 7:00 PM, Ross Paterson
On Tue, Apr 06, 2010 at 05:18:34PM -0400, Job Vranish wrote:
So in Haskell 98, would the added constraints result in a type error?
Yes, because the types of the mutually recursive identifiers would be inferred together without using the type signatures, and then would fail to match the declared types.
But then there aren't any implementations of Haskell 98 to test this on. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Yes, it has to do with mutually recursive bindings. If you add a type
signature, you break the mutual recursion. Mutually recursive
functions are type-checked together and then generalised. Similarly,
polymorphic recursion cannot be inferred either, but is possible by
adding a type signature.
HTH
On 6 April 2010 20:56, Job Vranish
Is haskell supposed to always infer the most general type (barring extensions)?
I found a simple case where this is not true:
f _ = undefined where _ = y :: Int -> Int
y x = undefined where _ = f x
Haskell infers the types of 'y' and 'f' as: f :: Int -> a y :: Int -> Int
This confused me at first, but after thinking about it a while it seemed to make sense. But then my friend John pointed out that you can add type sigs for 'f' and 'y': f :: a -> b y :: a -> b and have it still typecheck!
This thoroughly confused me.
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 :)
- Job
_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- Push the envelope. Watch it bend.
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/
participants (7)
-
Brandon S. Allbery KF8NH -
Edward Z. Yang -
Job Vranish -
John Meacham -
John Van Enk -
Ross Paterson -
Thomas Schilling