On Tue, 2008-05-27 at 01:45 +0100, Eric Stansifer wrote:
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/.
It's not "carrying a forall" around with it. The fact that 'a' is otherwise unbound leads GHC to insert a 'forall a'. That's another way in which forall and class constraints aren't remotely the same. forall is a binding construct that introduces a new type variable, a class constraint is not a binding construct.
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?
Doesn't work for me either which kind of relieves me as I don't particularly like that interpretation.