[Haskell-cafe] Aren't type system extensions fun?
derek.a.elkins at gmail.com
Mon May 26 21:11:36 EDT 2008
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
> ((F a, C1 a) => a -> a) is to (C1 a => a -> a)
> (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 22.214.171.124 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.
More information about the Haskell-Cafe