[Haskell-cafe] Aren't type system extensions fun? [Further
analysis]
Kim-Ee Yeoh
a.biurvOir4 at asuhan.com
Tue May 27 15:40:34 EDT 2008
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.
More information about the Haskell-Cafe
mailing list