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
Ben Rudiak-Gould wrote:
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.
I'd quite like to see a flag that switches off implicit "forall" quantification altogether, or maybe just warned about it (since I use -Wall -Werror anyway). id :: forall a. a -> a const :: forall a b. a -> b -> a etc.
On Tue, Feb 07, 2006 at 08:15:19PM +0000, Ben Rudiak-Gould wrote:
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.
A second problem with GHC's provision of scoped type variables is the confusing variety of ways of doing it. Some of them address the same problem that partial type signatures aim at (e.g. by allowing signatures for parts of arguments and/or the result of functions). Partial type signatures may well not be ready in time for Haskell', but we should still try to avoid overlap. I think we should "do the simplest thing that could possibly work", and then see if we really need more. By "work", I mean a compatible extension of H98 that makes it possible to add type signatures for local bindings (which isn't always possible in H98). How about: * no implicit binding of type variables: to bind, use "forall". * pattern type annotations allowed only at the top level of pattern bindings and lambda arguments (not on sub-patterns or arguments of function bindings). * no result type annotations (except on pattern bindings, where they're equivalent to top-level pattern type annotations).
I wrote:
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. [...]
Here's a completely different idea for solving this. It occurs to me that there isn't all that much difference between capitalized and lowercase identifiers in the type language. One set is for type constants and the other for type variables, but one man's variable is another man's constant, as the epigram goes. In Haskell 98 type signatures, the difference between them is precisely that type variables are bound within the type, and type constants are bound in the environment. Maybe scoped type variables should be capitalized. At the usage point this definitely makes sense: you really shouldn't care whether the thing you're pulling in from the environment was bound at the top level or in a nested scope. And implicit quantification does the right thing. As for binding, I suppose the simplest solution would be explicit quantification of the capitalized variables, e.g. f :: forall N. [N] -> ... f x = ... or f (x :: exists N. [N]) = ... Really, the latter binding should be in the pattern, not in the type signature, but that's trickier (from a purely syntactic standpoint). What do people think of this? I've never seen anyone suggest capitalized type variables before, but it seems to make sense. -- Ben
participants (3)
-
Ashley Yakeley -
Ben Rudiak-Gould -
Ross Paterson