OK, OK, I yield! This message is about lexically scoped type variables. I've gradually become convinced that if you write f :: [a] -> [a] f x = <body> then the type variable 'a' should be in scope in <body>. At present in GHC you have to write f (x :: [a]) = <body> to bring 'a' into scope. I've fought against this because it seems funny for a 'forall' in a type signature to bring a type variable into scope in perhaps-distant function body, but it's just so convenient and "natural". Furthermore, as Martin Sulzmann points out, you might have type variables that are mentioned only in the context of the type: g :: Foo a b => [a] -> [a] g = ... GHC provides no way to bring 'b' into scope at the moment, and that seems bad design. If I do this, which I'm inclined to, it could break some programs, because (with -fglasgow-exts) all type signatures will bring scoped type variables into scope in their function body. Here's an example that will break f :: [a] -> [a] f x = my_id x where my_id :: a -> a my_id y = y The type signature for my_id will become monomorphic, since 'a' is now in scope, so the application (my_id x) will fail saying can't unify 'a' with '[a]'. In some ways that makes sense. If you used 'b' instead in the defn of my_id, it'd be fine, because my_id would get the type (forall b. b->b). Fixing such breakages is easy. So there it is. Any one have strong opinions? (This is in addition to the existing mechanism for bringing scoped type variables into scope via pattern type signatures, of course.) Simon
On 2004-12-17 at 17:51GMT "Simon Peyton-Jones" wrote:
This message is about lexically scoped type variables.
I've been trying to work out what I think about this since you sent out the first message in this thread. I'm not sure that I've come to a useful conclusion, so I'll summarise my thoughts and see if that makes anything pop out of someone else's head. First, I've never liked the fact that type variables in signatures aren't declared anywhere -- this was part of the motivation that drove me to use a non-Hindley-Milner type system in Ponder. There, you could put a quantifier on an expression, so instead of
f :: [a] -> [a] f x = <body>
you could write (mangled to make it look more like Haskell) stuff like f = forall a.\(x::[a]) -> <body>::[a] and the scope of a was completely clear. Of course, this doesn't work with the way variables are declared in Haskell. Would it help to stick the quantifier at the beginning of the type declaration?
forall a b . g :: Foo a b => [a] -> [a] g = ...
That reads OK, and one can imagine that whenever you see a "g = ..." bit, you implicitly get the type variables that come at the front of the type declaration in scope as well. Doing this would mean that you keep the old behaviour for cases where there is no quantifier at the beginning of the type declaration, so things wouldn't break.
So there it is. Any one have strong opinions? (This is in addition to the existing mechanism for bringing scoped type variables into scope via pattern type signatures, of course.)
If I have a strong opinion about anything it's that the only thing that should bring type variables into scope is a(n implied) quantifier. Free variables are nasty. I don't hold out much hope of convincing anyone of this last, though. Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk
what about having -fno-lexically-scoped-types for old code? Keean. Simon Peyton-Jones wrote:
OK, OK, I yield!
This message is about lexically scoped type variables. I've gradually become convinced that if you write
f :: [a] -> [a] f x = <body>
then the type variable 'a' should be in scope in <body>. At present in GHC you have to write f (x :: [a]) = <body> to bring 'a' into scope.
I've fought against this because it seems funny for a 'forall' in a type signature to bring a type variable into scope in perhaps-distant function body, but it's just so convenient and "natural". Furthermore, as Martin Sulzmann points out, you might have type variables that are mentioned only in the context of the type: g :: Foo a b => [a] -> [a] g = ... GHC provides no way to bring 'b' into scope at the moment, and that seems bad design.
If I do this, which I'm inclined to, it could break some programs, because (with -fglasgow-exts) all type signatures will bring scoped type variables into scope in their function body. Here's an example that will break
f :: [a] -> [a] f x = my_id x where my_id :: a -> a my_id y = y
The type signature for my_id will become monomorphic, since 'a' is now in scope, so the application (my_id x) will fail saying can't unify 'a' with '[a]'. In some ways that makes sense. If you used 'b' instead in the defn of my_id, it'd be fine, because my_id would get the type (forall b. b->b). Fixing such breakages is easy.
So there it is. Any one have strong opinions? (This is in addition to the existing mechanism for bringing scoped type variables into scope via pattern type signatures, of course.)
Simon _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Please! I've lost count of the number of times when I've written code as
f :: a -> b
f (x :: a) = ...
wishing that I didn't have to locally bind the 'a'.
I'm not sure I understand the objection raised by Jon; the 'implicit
declaration' of type variables in type signatures has never bothered
me, and in fact seems quite similar to how names for values don't have
to be declared beforehand but are brought into scope by the binding
(which I also have no problem with).
Abe
On Fri, 17 Dec 2004 19:37:00 +0000, Keean Schupke
what about having -fno-lexically-scoped-types for old code?
Keean.
Simon Peyton-Jones wrote:
OK, OK, I yield!
This message is about lexically scoped type variables. I've gradually become convinced that if you write
f :: [a] -> [a] f x = <body>
then the type variable 'a' should be in scope in <body>. At present in GHC you have to write f (x :: [a]) = <body> to bring 'a' into scope.
I've fought against this because it seems funny for a 'forall' in a type signature to bring a type variable into scope in perhaps-distant function body, but it's just so convenient and "natural". Furthermore, as Martin Sulzmann points out, you might have type variables that are mentioned only in the context of the type: g :: Foo a b => [a] -> [a] g = ... GHC provides no way to bring 'b' into scope at the moment, and that seems bad design.
If I do this, which I'm inclined to, it could break some programs, because (with -fglasgow-exts) all type signatures will bring scoped type variables into scope in their function body. Here's an example that will break
f :: [a] -> [a] f x = my_id x where my_id :: a -> a my_id y = y
The type signature for my_id will become monomorphic, since 'a' is now in scope, so the application (my_id x) will fail saying can't unify 'a' with '[a]'. In some ways that makes sense. If you used 'b' instead in the defn of my_id, it'd be fine, because my_id would get the type (forall b. b->b). Fixing such breakages is easy.
So there it is. Any one have strong opinions? (This is in addition to the existing mechanism for bringing scoped type variables into scope via pattern type signatures, of course.)
Simon _______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
I'm not sure I understand the objection raised by Jon; the 'implicit declaration' of type variables in type signatures has never bothered me, and in fact seems quite similar to how names for values don't have to be declared beforehand but are brought into scope by the binding (which I also have no problem with).
The binding of a variable is the declaration of the variable. In contrast, type variables are never declared in Haskell 98, they are only used. In my opinion this lack of an explicit type variable quantifier is just acceptable, because all type variables are universally quantified and their scope is just the type in which they appear. The very moment you allow for wider scopes of type variables the disadvantage of the lacking type variable quantifier becomes appearant: When you see f :: a -> a somewhere within an inner "where" clause you do not know at all if this means f :: forall a. a -> a or the "a" is actually quantified somewhere outside and hence "f" has a far more restricted type (because Haskell does not even require you to write a type signature next to its variable binding, you have to search the *whole* module to find out). So scoped type variables do not fit Haskell well anyway, but I think when added they should at least be an upward compatible extension; any Haskell 98 program should still be correct. Hence I support Jon in that ghc should only allow those type variables a wider scope that have been explicitly declared with the non-Haskell 98 keyword "forall". Olaf
Hi all, Olaf Chitil wrote:
Hence I support Jon in that ghc should only allow those type variables a wider scope that have been explicitly declared with the non-Haskell 98 keyword "forall".
I'm inclined to support Jon and Olaf here. I'm pretty sure there's lot of code out there that use "-fglasgow-exts" for all sorts of reasons totally unrelated to scoped type variables. Moreover, I suspect that type signatures for local definitions are quite common too. I, at least, use them a fair bit. So, unless it is 100% clear that the proposed additional way of introducing scoped type variables really is the way to go, I would say go for the version that breaks the fewest programs. If nothing else, if it does turn out to really be the right way, it would seem fairly easy to later generalize the rule, by not requiring an explicit forall (and thus recovering the property that the current type signature syntax is just a syntactic shorthand) than go the other way. Personally, I always get a bit worried when there is too much "magic" going on, e.g. when the meaning of syntactic constructs are stretched in various ways in attempts to "do the right thing" tacitly. I believe it usually better, in the long run at least, to state intentions more explicitly. E.g., in this case, maybe it isn't such a bad idea after all to differentiate syntactically between binding occurrences and referring occurrences of scoped type variables? Thus, also from this perspective it would seem that requiring an explicit forall for introducing scoped type variables would be the better option as it could be argued that intentions are stated a bit more explicitly that way, although maybe not in as explicitly as could be desired. It is, however, unfortunate that a signature without outer foralls no longer would be just a syntactic shorthand for signatures with the foralls mentioned explicitly. Best regards, /Henrik -- Henrik Nilsson School of Computer Science and Information Technology The University of Nottingham nhn@cs.nott.ac.uk This message has been scanned but we cannot guarantee that it and any attachments are free from viruses or other damaging content: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.
On 18/12/2004, at 4:51 AM, Simon Peyton-Jones wrote:
This message is about lexically scoped type variables. I've gradually become convinced that if you write
f :: [a] -> [a] f x = <body>
then the type variable 'a' should be in scope in <body>.
I don't have a particularly strong opinion about this, but I've always thought that your suggestion is the way it should have been done. I actually find it confusing when someone "re-declares" the type variables in the function body; e.g. in your example of ...
f :: [a] -> [a] f x = my_id x where my_id :: a -> a my_id y = y
I would be very much inclined to use a type signature of "my_id :: b -> b", which makes it 100% obvious that it's using a fresh type variable. Considering that normal variables are lexically scoped, it seems intuitive to me that type variables should also be lexically scoped. -- % Andre Pang : trust.in.love.to.save
participants (7)
-
Abraham Egnor -
Andre Pang -
Henrik Nilsson -
Jon Fairbairn -
Keean Schupke -
Olaf Chitil -
Simon Peyton-Jones