Hello, GHC 6.12.3 allows to omit the explicit quantification of higher-rank type variables using 'forall' in data types if they appear in a type class context {-# LANGUAGE RankNTypes #-} data Foo = Foo (Eq a => a) Is this implicit introduction of 'forall' intended? If it is, why does it not work in function types? The following is not accepted by my GHC: bar :: Eq b => (Eq a => a) -> b bar x = x The error message is All of the type variables in the constraint `Eq a' are already in scope (at least one must be universally quantified here) (Use -XFlexibleContexts to lift this restriction) Using `FlexibleContexts` the signature of `bar` seems to be interpreted as bar :: (Eq b, Eq a) => a -> b because then the error becomes Couldn't match expected type `b' against inferred type `a' So unlike in data-type declarations, a 'forall' in a function type must be written explicitly even if the quantified variable appears in a local type class constraint. bar :: Eq b => (forall a . Eq a => a) -> b bar x = x I have not yet installed GHC 7. Is this inconsistency between data and function declarations intended or has it been changed in the new type checker? Sebastian
The current story is this: GHC adds an implicit "forall" at the top of every type that foralls all the type variables mentioned in the type that are not already in scope (if lexically scoped tyvars is on) This is stated pretty clearly here http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/other-type-extension... Thus, when you write bar :: Eq b => (Eq a => a) -> b you get bar :: forall a b. Eq b => (Eq a => a) -> b In a data type decl data Foo = Foo (Eq a => a) the "top of the type" is done separately for each argument. After all, Foo (Eq a => a) isn't a type. So you get data Foo = Foo (forall a. Eq a => a) So that's what happens. You could imagine a different design, in which an implicit 'forall' is added at each "=>", forall'ing any not-otherwise-bound type variables. So if you said bar :: Eq b => (Eq a => a) -> b you'd get bar :: forall b. Eq b => (forall a. Eq a => a) -> b But it's not obvious that's what you want. Suppose you wrote bar :: (Eq a => a) -> a Then which of these two do you want? bar :: forall a. (forall a. Eq a => a) -> a bar :: forall a. (Eq a => a) -> a And then what's the rule lexically scoped tyvars? I hope that explains it. The documentation mentioned above has examples. I'll gladly improve it if you can suggest concrete wording. Simon | -----Original Message----- | From: glasgow-haskell-users-bounces@haskell.org [mailto:glasgow-haskell-users- | bounces@haskell.org] On Behalf Of Sebastian Fischer | Sent: 16 October 2010 02:10 | To: GHC Users | Subject: Implicit 'forall' in data declarations | | Hello, | | GHC 6.12.3 allows to omit the explicit quantification of | higher-rank type variables using 'forall' in data types if they | appear in a type class context | | {-# LANGUAGE RankNTypes #-} | data Foo = Foo (Eq a => a) | | Is this implicit introduction of 'forall' intended? If it is, why | does it not work in function types? The following is not accepted | by my GHC: | | bar :: Eq b => (Eq a => a) -> b | bar x = x | | The error message is | | All of the type variables in the constraint `Eq a' | are already in scope (at least one must be universally quantified | here) | (Use -XFlexibleContexts to lift this restriction) | | Using `FlexibleContexts` the signature of `bar` seems to be | interpreted as | | bar :: (Eq b, Eq a) => a -> b | | because then the error becomes | | Couldn't match expected type `b' against inferred type `a' | | So unlike in data-type declarations, a 'forall' in a function type | must be written explicitly even if the quantified variable appears in | a local type class constraint. | | bar :: Eq b => (forall a . Eq a => a) -> b | bar x = x | | I have not yet installed GHC 7. Is this inconsistency between data and | function declarations intended or has it been changed in the new type | checker? | | Sebastian | _______________________________________________ | Glasgow-haskell-users mailing list | Glasgow-haskell-users@haskell.org | http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Hi Simon, thank you for your explanations. Now I understand why type variables are quantified at the outermost position in function types. My confusion was caused by implicit quantifications in data type declarations. These are not (explicitly) mentioned in the documentation that you have linked and they only occur when a type class context is given.
In a data type decl data Foo = Foo (Eq a => a) the "top of the type" is done separately for each argument. After all, Foo (Eq a => a) isn't a type. So you get data Foo = Foo (forall a. Eq a => a)
This was a surprise as data Bar = Bar (a -> a) is illegal and *not* equivalent to data Bar = Bar (forall a . a -> a) (at least in GHC 6.12.3) This lead me into thinking that the type class context causes quantification which was apparently wrong. In fact, I think according to the documentation of implicit quantification it is unclear if the definitions of Foo and Bar (without explicit forall) are legal. I expected both to be illegal and am surprised that one is legal and the other is not. If "the top level of user written types" includes data constructor arguments, then probably both should be legal. On the other hand it would probably be surprising if one could write data Id type = Id typ without getting an error message.
Suppose you wrote
bar :: (Eq a => a) -> a
Then which of these two do you want?
bar :: forall a. (forall a. Eq a => a) -> a bar :: forall a. (Eq a => a) -> a
And then what's the rule lexically scoped tyvars?
I'm afraid I don't understand your question. But I'm fine with the current behaviour of implicit quantification in function types. Sebastian
| > In a data type decl | > data Foo = Foo (Eq a => a) | > the "top of the type" is done separately for each argument. After | > all, Foo (Eq a => a) isn't a type. So you get | > data Foo = Foo (forall a. Eq a => a) | | This was a surprise as | | data Bar = Bar (a -> a) | | is illegal and *not* equivalent to | | data Bar = Bar (forall a . a -> a) Darn, that's quite right. In fact what really happens is that the "top of a type" thing is triggered by a "=>", which is why Bar (a->a) is treated differently than Bar (Eq a => a -> a). The rule I originally gave would indeed treat data Bar a = Bar aa as meaning data Bar a = Bar (forall aa. aa) which is almost certainly not right. So GHC's behaviour is probably about right, but the description is wrong. Let's try again: A "implicit quantification point" is a) the type in a type signature f :: type, or b) a type of form (context => type), that is not enclosed by an explicit 'forall' At each implicit quantification point 'ty', working outside in, GHC finds all the type variables a,b,c in 'ty' that are not already in scope, and transforms 'ty' to (forall a,b,c. ty). Note that * the argument of a constructor is not an implicit quantification point * implicit quantification points may be nested but the inner ones are effectively no-ops. Example f :: Int -> (Eq a => a -> a) -> Int There are two quantification points: the whole type, and the (Eq a => ...) But when the outer quantification point wraps forall a around it, the inner quantification point has no free variables to quantify. So we get f :: forall a. Int -> (Eq a => a -> a) -> Int Is that better? Simon | | (at least in GHC 6.12.3) | | This lead me into thinking that the type class context causes | quantification which was apparently wrong. | | In fact, I think according to the documentation of implicit | quantification it is unclear if the definitions of Foo and Bar | (without explicit forall) are legal. I expected both to be illegal and | am surprised that one is legal and the other is not. | | If "the top level of user written types" includes data constructor | arguments, then probably both should be legal. On the other hand it | would probably be surprising if one could write | | data Id type = Id typ | | without getting an error message. | | > Suppose you wrote | > | > bar :: (Eq a => a) -> a | > | > Then which of these two do you want? | > | > bar :: forall a. (forall a. Eq a => a) -> a | > bar :: forall a. (Eq a => a) -> a | > | > And then what's the rule lexically scoped tyvars? | | I'm afraid I don't understand your question. But I'm fine with the | current behaviour of implicit quantification in function types. | | Sebastian
On Oct 21, 2010, at 9:58 PM, Simon Peyton-Jones wrote:
A "implicit quantification point" is a) the type in a type signature f :: type, or b) a type of form (context => type), that is not enclosed by an explicit 'forall'
not quite: foo :: forall a . a -> (Ord b => b) -> () According to your explanation, there is one implicit quantification point: the whole type of `foo`. The type `Ord b => b` is no implicit quantification point because it is "enclosed by" an explicit 'forall' (for a certain definition of "enclosed by"). The new explanation implies that the type should be foo :: forall b . forall a . a -> (Ord b => b) -> () but it is foo :: forall a . a -> (forall b . Ord b => b) -> () instead. Apparently, if there is an explicit 'forall' (that does not mention `b`) then the implicit 'forall' is inserted at the context. If there is no explicit 'forall' then it is inserted at the top level. My impression is the following: An implicit quantification point is a) the type in a type signature f :: type or b) a type of the form (context => type) if it does not start with an explicit 'forall' Then the only implicit quantification point in the type of `foo` is the type `Ord b => b` which matches the behaviour of GHC. Is this what you meant? Sebastian
On Oct 21, 2010, at 11:14 PM, Sebastian Fischer wrote:
An implicit quantification point is a) the type in a type signature f :: type or b) a type of the form (context => type) if it does not start with an explicit 'forall'
According to this explanation, the type bar :: forall . (Ord a => a) -> () means bar :: (forall . Ord a => a) -> () which it actually does. Sebastian
On Oct 21, 2010, at 9:58 PM, Simon Peyton-Jones wrote:
So GHC's behaviour is probably about right, but the description is wrong.
On Oct 21, 2010, at 11:14 PM, Sebastian Fischer wrote:
An implicit quantification point is a) the type in a type signature f :: type or b) a type of the form (context => type) if it does not start with an explicit 'forall'
I have mixed feelings about b). A special treatment of contexts is convenient but also confusing because they are treated differently depending on where they occur. It is convenient because one can omit 'forall's in higher-rank types if they use contexts. It is confusing because types with context in type signatures are treated differently than types with context in data declarations (because type signatures are implicit quantification points and arguments in data declarations are not.) How inconvenient would it be to make the above description simpler by dropping b) and thus require more explicit 'forall's? I don't know what I prefer. I like both convenience and simplicity of explanations and cannot judge wich alternative has more convincing arguments in this case. Sebastian
| > An implicit quantification point is | > a) the type in a type signature f :: type or | > b) a type of the form (context => type) | > if it does not start with an explicit 'forall' | ... | How inconvenient would it be to make the above description simpler by | dropping b) and thus require more explicit 'forall's? I don't know | what I prefer. I like both convenience and simplicity of explanations | and cannot judge wich alternative has more convincing arguments in | this case. It'd be easy to implement, and now you've forced me to realise that the current rule is quite tricky to explain, I think it'd be an improvement to drop (b). But it's an unforced change and some programs would require fixing. Does anyone listening to this thread have an opinion? Just to summarise, Sebastian's proposal is that Haskell's implicit quantification (adding foralls) would occur *only* right at the top of a type signature. The only observable differences in behaviour would, I believe be these * In a data type declaration data Foo = MkFoo (Eq a => a -> a) you'd get an error "a is not in scope", just as you would with data Foo = MkFoo (a->a) * Inside an *explicit* forall you would get no *implicit* foralls: f :: forall a. (Eq b => b->b) -> a -> a would yield "b is not in scope", whereas at present it behaves like f :: forall a. (forall b. Eq b => b->b) -> a -> a I vote for this. In fact I've created a ticket for it. http://hackage.haskell.org/trac/ghc/ticket/4426 Others listening to this thread: what do you think? Add a comment to the ticket. Simon
On Oct 22, 2010, at 5:20 PM, Simon Peyton-Jones wrote:
I vote for this. In fact I've created a ticket for it. http://hackage.haskell.org/trac/ghc/ticket/4426
+1 (I decided to prefer simplicity over convenience in this case) Sebastian
On Fri, Oct 22, 2010 at 4:20 AM, Simon Peyton-Jones
Does anyone listening to this thread have an opinion? Just to summarise, Sebastian's proposal is that Haskell's implicit quantification (adding foralls) would occur *only* right at the top of a type signature.
Before this discussion, I thought things already worked the way you
describe in your proposal.
On a related note, these are also apparently allowed (in 6.10.4):
f :: forall a. (Eq a => a -> a) -> a -> a
-- the Eq context prevents the function from ever being called.
g :: forall a. Ord a => (Eq a => a -> a) -> a -> a
-- the Eq context is effectively ignored
Up until now, I thought contexts were only allowed after a forall
(explicit or implicit), and I can't really think of a reason to have
one anywhere else.
My suggestion would be either
(1) forbid contexts, except after foralls, and only implicitly add
foralls at the top of the type
(2) add implicit foralls before any context, even if the variables are
already in scope
--
Dave Menendez
| On a related note, these are also apparently allowed (in 6.10.4): | f :: forall a. (Eq a => a -> a) -> a -> a | -- the Eq context prevents the function from ever being called. That's not true. E.g. f ((==) True) True works fine. | g :: forall a. Ord a => (Eq a => a -> a) -> a -> a | -- the Eq context is effectively ignored That's a bit more true, because Ord a implies Eq a, but still not really. It still says that you must pass evidence for equality to g's argument. Simon
On Mon, Oct 25, 2010 at 3:16 AM, Simon Peyton-Jones
| On a related note, these are also apparently allowed (in 6.10.4): | f :: forall a. (Eq a => a -> a) -> a -> a | -- the Eq context prevents the function from ever being called.
That's not true. E.g. f ((==) True) True works fine.
What I meant is that f cannot call its argument. That is, f :: forall a. (Eq a => a -> a) -> a -> a f g x = g x is ill-typed.
| g :: forall a. Ord a => (Eq a => a -> a) -> a -> a | -- the Eq context is effectively ignored
That's a bit more true, because Ord a implies Eq a, but still not really. It still says that you must pass evidence for equality to g's argument.
Is that different from forall a. Ord a => (a -> a) -> a -> a?
--
Dave Menendez
| > | On a related note, these are also apparently allowed (in 6.10.4): | > | f :: forall a. (Eq a => a -> a) -> a -> a | > | -- the Eq context prevents the function from ever being called. | > | > That's not true. E.g. | > f ((==) True) True | > works fine. | | What I meant is that f cannot call its argument. Oh now I see. Yes, that's true. But it could be hard to work out: f :: forall a. (C a, D a) => (E [a] => a -> a) -> Int Can 'f' call its argument? Well, it depends if you can deduce E [a] from (C a, D a). And if this was a local type signature there might be other constraints in scope. Anyway, it's certainly true that some types are more useful than others (e.g. (forall a. Int -> a) must be the constant bottom function), but I don't think it's fruitful to try to exclude them *as types*. Simon
participants (3)
-
David Menendez -
Sebastian Fischer -
Simon Peyton-Jones