Simon PJ thinks that Haskell' should include scoped type variables, and I
tend to agree. But I'm unhappy with one aspect of the way they're
implemented in GHC. What I don't like is that given a signature like
x :: a -> a
there's no way to tell, looking at it in isolation, whether a is free or
bound in the type. Even looking at the context it can be hard to tell,
because GHC's scoping rules for type variables are fairly complicated and
subject to change. This situation never arises in the expression language or
in Haskell 98's type language, and I don't think it should arise in Haskell
at all.
What I'd like to propose is that if Haskell' adopts scoped type variables,
they work this way instead:
1. Implicit forall-quantification happens if and only if the type does
not begin with an explicit forall. GHC almost follows this rule,
except that "forall." (with no variables listed) doesn't suppress
implicit quantification---but Simon informs me that this is a bug
that will be fixed.
2. Implicit quantification quantifies over all free variables in the
type, thus closing it. GHC's current behavior is to quantify over
a type variable iff there isn't a type variable with that name in
scope.
Some care is needed in the case of class method signatures: (return :: a ->
m a) is the same as (return :: forall a. a -> m a) but not the same as
(return :: forall a m. a -> m a). On the other hand the practical type of
return as a top-level function is (Monad m => a -> m a), which is the same
as (forall m a. Monad m => a -> m a), so this isn't quite an exception
depending on how you look at it. I suppose it is a counterexample to my
claim that Haskell 98's type language doesn't confuse free and bound
variables, though.
If rule 2 were accepted into Haskell' and/or GHC, then code which uses
implicit quantification and GHC scoped type variables in the same type would
have to be changed to explicitly quantify those types; other programs
(including all valid Haskell 98 programs) would continue to work unchanged.
Note that the signature "x :: a", where a refers to a scoped type variable,
would have to be changed to "x :: forall. a", which is potentially
confusable with "x :: forall a. a"; maybe the syntax "forall _. a" should be
introduced to make this clearer. The cleanest solution would be to abandon
implicit quantification, but I don't suppose anyone would go for that.
With these two rules in effect, there's a pretty good case for adopting rule 3:
3. Every type signature brings all its bound type variables into scope.
Currently GHC has fairly complicated rules regarding what gets placed into
scope: e.g.
f :: [a] -> [a]
f = ...
brings nothing into scope,
f :: forall a. [a] -> [a]
f = ...
brings a into scope,
f :: forall a. [a] -> [a]
(f,g) = ...
brings nothing into scope (for reasons explained in [1]), and
f :: forall a. (forall b. b -> b) -> a
f = ...
brings a but not b into scope. Of course, b doesn't correspond to any type
that's accessible in its lexical scope, but that doesn't matter; it's
probably better that attempting to use b fail with a "not available here"
error message than that it fail with a "no such type variable" message, or
succeed and pull in another b from an enclosing scope.
There are some interesting corner cases. For example, rank-3 types:
f :: ((forall a. a -> X) -> Y) -> Z
f g = g (\x -> <exp>)
should a denote x's type within <exp>? It's a bit strange if it does, since
the internal System F type variable that a refers to isn't bound in the same
place as a itself. It's also a bit strange if it doesn't, since the
identification is unambiguous.
What about shadowing within a type:
f :: forall a. (forall a. a -> a) -> a
I can't see any reason to allow such expressions in the first place.
What about type synonyms with bound variables? Probably they should be
alpha-renamed into something inaccessible. It seems too confusing to bring
them into scope, especially since they may belong to another module and this
would introduce a new notion of exporting type variables.
I like rule 3 because of its simplicity, but a rule that, say, brought only
rank-1 explicitly quantified type variables into scope would probably be
good enough. Rules 1 and 2 seem more important. I feel like a new language
standard should specify something cleaner and more orthogonal than GHC's
current system.
-- Ben
[1]http://www.mail-archive.com/glasgow-haskell-users@haskell.org/msg09117.html
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime
