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

[Luke Palmer]

On Tue, May 27, 2008 at 5:55 PM, Andrew Coppin
<andrewcoppin at btinternet.com> wrote:
> 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.
>
> So what is the type of that second expression? You would think that
>
>  (x -> x) -> (Char, Bool)

When you're reasoning about this, I think it would help you greatly to
explicitly put in *all* the foralls.  In haskell, when you write, say:

   map :: (a -> b) -> [a] -> [b]

All the free variables are *implicitly* quantified at the top level.
That is, when you write the above, the compiler sees:

   map :: forall a b. (a -> b) -> [a] -> [b]

(forall has low precedence, so this is the same as:

   map :: forall a b. ((a -> b) -> [a] -> [b])

)

And the type you mention above for the strange expression is:

   forall x. (x -> x) -> (Char, Bool)

Which indicates that the caller gets to choose.  That is, if a caller
sees a 'forall' at the top level, it is allowed to instantiate it with
whatever type it likes.   Whereas the type you want has the forall in
a different place than the implicit quantifiaction:

   (forall x. x -> x) -> (Char, Bool)

Here the caller does not have a forall at the top level, it is hidden
inside a function type so the caller cannot instantiate the type.
However, when implementing this function, the argument will now have
type

    forall x. x -> x

And the implementation can instantiate x to be whatever type it likes.

But my strongest advice is, when you're thinking through this, remember that:

   x -> x

Is not by itself a type, because x is meaningless.   Instead it is
Haskell shorthand for

   forall x. x -> x

Luke

> 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.
>
> 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.
>
> 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:
>
> - A function starts out with a polymorphic type, such as 'x -> x'.
>
> - Each time the function is called, all the type variables have to be locked
> down to real types such as 'Int' or 'Either (Maybe (IO Int)) String' or
> something.
>
> - By the above, any function passed to a high-order function has to have all
> its type variables locked down, yielding a completely monomorphic function.
>
> - In the exotic case above, we specifically WANT a polymorphic function,
> hence the problem.
>
> - The "forall" hack somehow convinces the type checker to not lock down some
> of the type variables. In this way, the type variables relating to a
> function can remain unlocked until we reach each of the call sites. This
> allows the variables to be locked to different types at each site [exactly
> as they would be if the function were top-level rather than an argument].
>
> This is a plausible hypothesis for what this language feature actually does.
> [It is of course frustrating that I have to hypothesise rather than read a
> definition.] However, this still leaves a large number of questions
> unanswered...
>
> - Why are top-level variables and function arguments treated differently by
> the type system?
> - Why do I have to manually tell the type checker something that should be
> self-evident?
> - Why do all type variables need to be locked down at each call site in the
> first place?
> - Why is this virtually never a problem in real Haskell programs?
> - Is there ever a situation where the unhacked type system behaviour is
> actually desirably?
> - 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?
>
>
>
> Unfortunately, the GHC manual doesn't have a lot to say on the matter.
> Reading section 8.7.4 ("Arbitrary-rank polymorphism"), we find the
> following:
>
> - "The type 'x -> x' is equivilent to 'forall x. x -> x'." [Um... OK, that's
> nice?]
>
> - "GHC also allows you to do things like 'forall x. x -> (forall y. y ->
> y)'." [Fascinating, but what does that MEAN?]
>
> - "The forall makes explicit the universal quantification that is implicitly
> added by Haskell." [Wuh??]
>
> - "You can control this feature using the following language options..."
> [Useful to know, but I still don't get what this feature IS.]
>
> The examples don't help much either, because (for reasons I haven't figured
> out yet) you apparently only need this feature in fairly obscure cases.
>
> The key problem seems to be that the GHC manual assumes that anybody reading
> it will know what "universal quantification" actually means. Unfortunately,
> neither I nor any other human being I'm aware of has the slightest clue what
> that means. A quick search on that infallable reference [sic] Wikipedia
> yields several articles full of dense logic theory. Trying to learn brand
> new concepts from an encyclopedia is more or less doomed from the start. As
> far as I can comprehend it, we have
>
>  existential quantification = "this is true for SOMETHING"
>  universal quantification = "this is true for EVERYTHING"
>
> Quite how that is relevant to the current discussion eludes me.
>
> I have complete confidence that whoever wrote the GHC manual knew exactly
> what they meant. I am also fairly confident that this was the same person
> who implemented and even designed this particular feature. And that they
> probably have an advanced degree in type system theory. I, however, do not.
> So if in future the GHC manual could explain this in less opaque language,
> that would be most appreciated. :-}
>
> For example, the above statements indicate that '(x -> x) -> (Char, Bool)'
> is equivilent to 'forall x. (x -> x) -> (Char, Bool)', and we already know
> that this is NOT the same as '(forall x. x -> x) -> (Char, Bool)'. So
> clearly my theory above is incomplete, because it fails to explain why this
> difference exists. My head hurts...
>
> (Of course, I could just sit back and pretend that rank-N types don't exist.
> But I'd prefer to comprehend them if possible...)
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>