[Haskell-cafe] Aren't type system extensions fun?

[Eric Stansifer]

>> Say, wouldn't a syntax like "(forall a => a -> a)" or "(a => a -> a)"
>> or something similar to that be more consistent with syntax for
>> contexts, e.g. "(Ord a => a -> a)"?
>
> It's not remotely the same thing as a class constraint so why would we
> want it to be "consistent" with it?

Well, true;  the idea come from when I read just now in the ghc manual
that the following are equivalent:

> data T = MkT (Ord a => a -> a)
> data U = MkU (forall a. Ord a => a -> a)

In other words, the context "Ord a" in the /T/ definition is
implicitly carrying a "forall a" around with it.  In a sense, one can
think of "forall a" as a class constraint for /a/ that offers no
constraints at all;  i.e., "forall a" is satisfied by any type /a/,
whereas "Ord a", for example, is satisfied by any type /a/ which has
an instance for /Ord/.

To be exact, here is the analogy I'm making.

Suppose we have:
> class F a => C1 a
> class C2 a

Then:
((F a, C1 a) => a -> a) is to (C1 a => a -> a)
as
(forall a. C2 a => a -> a) is to (C2 a => a -> a)

That is, /forall a/ acts like a constraint that always succeeds (and
is thus usually implicit -- e.g., in the line "class C2 a").

The analogy, of course, breaks down the moment one writes:

> -- t :: (Ord a => a -> a) -> T
> -- t = MkT
>
> u :: (forall a. Ord a => a -> a) -> U
> u = MkU

where for very good reasons the type signatures written for /t/ and
/u/ above mean entirely different things.

So, the similarity is rather tenuous, and is further diminished
because the "forall a" construct and the "Ord a" construct are used
for entirely different things in practice, regardless of some nice,
abstract connection that I see between them.  But I hope you see why I
feel that "forall a" is in some ways closely related to "Ord a".
[Incidentally, I also don't like introducing new syntax (though
introducing new syntax is better than abusing existing syntax).]



On another note:  the ghc 6.6.1 manual says (as does the latest
manual, but I have version 6.6.1, so that's what matters here) in
section 7.4.8.1 that the following are equivalent:

> data T a = MkT (Either a b) (b -> b)
> data T a = MkT (forall b. Either a b) (forall b. b -> b)

but for me, the first line does not compile with -fglasgow-exts (I
get:  "Not in scope:  type variable `b'"), but the second line does
compile.  Am I missing something here?

Eric