[Haskell-cafe] Re: Aren't type system extensions fun? [Further
ketil at malde.org
Wed May 28 01:29:36 EDT 2008
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
\f -> f 'J'
I think you'll agree this does not have type
(x->x) -> Char
(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 :-)
If I haven't seen further, it is by standing in the footprints of giants
More information about the Haskell-Cafe