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

[Chaddaï Fouché]

2008/5/27 Andrew Coppin <andrewcoppin at btinternet.com>:
> Gleb Alexeyev wrote:
>>
>> foo :: (forall a . a -> a) -> (Bool, String)
>> foo g = (g True, g "bzzt")
>
> 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.

No, this is a flaw in the type inferencer, but simply adding the
Rank-N type to our type system makes type inference undecidable.

I would argue against the "obviously perfectly type-safe" too since
most type system don't even allow for the second case.

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

None of the possible choice would be type-safe. This type means :
whatever the type a, function of type (a -> a) to a pair (Char, Bool)

But the type a is unique while in the body of your function, a would
need to be two different types.

> Interestingly, if you throw in the undocumented "forall" keyword, everything
> magically works:
>
>  (forall x. x -> x) -> (Char, Bool)
>
> Obviously, the syntax is fairly untidy. And the program is now not valid
> Haskell according to the written standard. And best of all, the compiler
> seems unable to deduce this type automatically either.

As I said, the compiler can't deduce this type automatically because
it would make type inference undecidable.

> 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. So far, the only really plausible theory I have been
> able to come up with is this:

Rank-N type aren't a "hack", they're perfectly understood and fit
nicely into the type system, their only problem is type inference.

> yada yada, complicated theory... cut

What you don't seem to understand is that "(x -> x) -> (Char, Bool)"
and "(forall x. x -> x) -> (Char, Bool)" are two very different
beasts, they aren't the same type at all !

Taking a real world situation to illustrate the difference :
Imagine you have different kind of automatic washer, some can wash
only wool while others can wash only cotton and finally some can wash
every kind of fabric...
You want to do business in the washing field but you don't have a
washer so you publish an announce :
If your announce say "whatever the type of fabric x, give me a machine
that can wash x and all you clothes and I'll give you back all your
clothes washed", the customer won't be happy when you will give him
back his wool clothes that the cotton washing machine he gave you torn
to shreds...
What you really want to say is "give me a machine that can wash any
type of fabric and your clothes and I'll give you back your clothes
washed".

The first announce correspond to "(x -> x) -> (Char, Bool)", the
second to "(forall x. x -> x) -> (Char, Bool)"

> - Why are top-level variables and function arguments treated differently by
> the type system?

They aren't (except if you're speaking about the monomorphism
restriction and that's another subject entirely).

> - Why do I have to manually tell the type checker something that should be
> self-evident?

Because it isn't in all cases to a machine, keep in mind you're an
human and we don't have real IA just yet.

> - Why is this virtually never a problem in real Haskell programs?

Because we seldom needs Rank-2 polymorphism.

> - Is there ever a situation where the unhacked type system behaviour is
> actually desirably?

Almost everytime. Taking a simple example : map
If the type of map was "(forall x. x -> x) -> [a] -> [a]", you could
only pass it "id" as argument, if it was "(forall x y. x -> y) -> [a]
-> [b]", you couldn't find a function to pass to it... (No function
has the type "a -> b")

> - Why can't the type system automatically detect where polymorphism is
> required?

It can and does, it can't detect Rank-N (N > 1) polymorphism because
it would be undecidable but it is fine with Rank-1 polymorphism (which
is what most people call polymorphism).

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

Maybe this should suggest to you that it is rather your understanding
of the question that is flawed... Haskell's type system is a fine
meshed mechanism that is soundly grounded in logic and mathematics, it
is rather unlikely that nobody would have noted the problem if it was
so important...

-- 
Jedaï