2008/5/27 Andrew Coppin
Gleb Alexeyev wrote:
foo :: (forall a . a -> a) -> (Bool, String) foo g = (g True, g "bzzt")
So, after an entire day of boggling my mind over this, I have brought it down to one simple example:
(id 'J', id True) -- Works perfectly.
\f -> (f 'J', f True) -- Fails miserably.
Both expressions are obviously perfectly type-safe, and yet the type checker stubbornly rejects the second example. Clearly this is a flaw in the type checker.
No, this is a flaw in the type inferencer, but simply adding the Rank-N type to our type system makes type inference undecidable. I would argue against the "obviously perfectly type-safe" too since most type system don't even allow for the second case.
So what is the type of that second expression? You would think that
(x -> x) -> (Char, Bool)
as a valid type for it. But alas, this is not correct. The CALLER is allowed to choose ANY type for x - and most of possible choices wouldn't be type-safe. So that's no good at all!
None of the possible choice would be type-safe. This type means : whatever the type a, function of type (a -> a) to a pair (Char, Bool) But the type a is unique while in the body of your function, a would need to be two different types.
Interestingly, if you throw in the undocumented "forall" keyword, everything magically works:
(forall x. x -> x) -> (Char, Bool)
Obviously, the syntax is fairly untidy. And the program is now not valid Haskell according to the written standard. And best of all, the compiler seems unable to deduce this type automatically either.
As I said, the compiler can't deduce this type automatically because it would make type inference undecidable.
At this point, I still haven't worked out exactly why this hack works. Indeed, I've spent all day puzzling over this, to the point that my head hurts! I have gone through several theories, all of which turned out to be self-contradictory. So far, the only really plausible theory I have been able to come up with is this:
Rank-N type aren't a "hack", they're perfectly understood and fit nicely into the type system, their only problem is type inference.
yada yada, complicated theory... cut
What you don't seem to understand is that "(x -> x) -> (Char, Bool)" and "(forall x. x -> x) -> (Char, Bool)" are two very different beasts, they aren't the same type at all ! Taking a real world situation to illustrate the difference : Imagine you have different kind of automatic washer, some can wash only wool while others can wash only cotton and finally some can wash every kind of fabric... You want to do business in the washing field but you don't have a washer so you publish an announce : If your announce say "whatever the type of fabric x, give me a machine that can wash x and all you clothes and I'll give you back all your clothes washed", the customer won't be happy when you will give him back his wool clothes that the cotton washing machine he gave you torn to shreds... What you really want to say is "give me a machine that can wash any type of fabric and your clothes and I'll give you back your clothes washed". The first announce correspond to "(x -> x) -> (Char, Bool)", the second to "(forall x. x -> x) -> (Char, Bool)"
- Why are top-level variables and function arguments treated differently by the type system?
They aren't (except if you're speaking about the monomorphism restriction and that's another subject entirely).
- Why do I have to manually tell the type checker something that should be self-evident?
Because it isn't in all cases to a machine, keep in mind you're an human and we don't have real IA just yet.
- Why is this virtually never a problem in real Haskell programs?
Because we seldom needs Rank-2 polymorphism.
- Is there ever a situation where the unhacked type system behaviour is actually desirably?
Almost everytime. Taking a simple example : map If the type of map was "(forall x. x -> x) -> [a] -> [a]", you could only pass it "id" as argument, if it was "(forall x y. x -> y) -> [a] -> [b]", you couldn't find a function to pass to it... (No function has the type "a -> b")
- Why can't the type system automatically detect where polymorphism is required?
It can and does, it can't detect Rank-N (N > 1) polymorphism because it would be undecidable but it is fine with Rank-1 polymorphism (which is what most people call polymorphism).
- Does the existence of these anomolies indicate that Haskell's entire type system is fundamentally flawed and needs to be radically altered - or completely redesigned?
Maybe this should suggest to you that it is rather your understanding of the question that is flawed... Haskell's type system is a fine meshed mechanism that is soundly grounded in logic and mathematics, it is rather unlikely that nobody would have noted the problem if it was so important... -- Jedaï