[Haskell-cafe] Re: Aren't type system extensions fun? [Further analysis]

[Ketil Malde]

Andrew Coppin <andrewcoppin at btinternet.com> writes:

> 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)

A bit late in the fray, but have you considered this simpler
expression: 

   \f -> f 'J'

I think you'll agree this does not have type 

  (x->x) -> Char

but rather

  (Char -> a) -> a

right?  Yet you can use 'id' as an argument (for f), since it has type 

        forall a . a -> a

where you are free to substitute Char for a and get (Char -> Char).

An expression like:

   \f -> (f 'J', f True)

requires an f that is both (Char -> a) and (Bool -> a) *at the same
time*.  A type like (a -> a) -> (Char,Bool) means that the expression
is polymorphic in its argument, but here you need to specify that the
function argument must be polymorphic itself.  

E.g. (forall a. a -> a) -> (Char,Bool). 

(Disclaimer: I hope I got it right :-)

-k
-- 
If I haven't seen further, it is by standing in the footprints of giants