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--tp17479349p17498362.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
