Andrew Coppin wrote:
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.
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!
In a nutshell, the function being passed MAY accept any type - but we want a function that MUST accept any type. This excusiatingly subtle distinction appears to be the source of all the trouble.
Let's fill in the type variable: (x -> x) -> (Char, Bool) ==> forall x. (x -> x) -> (Char, Bool) ==> x_t -> (x -> x) -> (Char, Bool), where x_t is the hidden type-variable, not unlike the reader monad. As you've pointed out, callER chooses x_t, say Int when passing in (+1) :: Int -> Int, which obviously would break \f -> (f 'J', f True). What we want is the callEE to choose x_t since callEE needs to instantiate x_t to Char and Bool. What we want is (x_t -> x -> x) -> (Char, Bool). But that's just (forall x. x -> x) -> (Char, Bool). For completeness' sake, let me just state that if universal quantification is like (x_t -> ...), then existential quantification is like (x_t, ...). Andrew Coppin wrote:
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.
My sympathies. You may find the haskell-cafe archive to be as useful as I have (search Ben Rudiak-Gould or Dan Licata). Having said that, I think you've done pretty well on your own. Andrew Coppin wrote:
- Why can't the type system automatically detect where polymorphism is required? - 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?
Well, give it a try! I'm sure I'm not the only one interested in your type inference experiments. Warning: they're addictive and may lead to advanced degrees and other undesirable side-effects. -- Kim-Ee -- View this message in context: http://www.nabble.com/Aren%27t-type-system-extensions-fun--tp17479349p174983... Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.