[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