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

[Derek Elkins]

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.