Hello,
On 1/26/07, Malcolm Wallace
[ scheme = 'forall' tvars '.' opt_ctxt type ] The non-terminal 'tvars' is a sequence of type variables that are separated by blank spaces. We have a choice if we should allow empty quantifier sequences. PROPOSAL: be liberal: * allow empty quantifier lists * allow variables that are not mentioned in the body of a type (but warn) * allow predicates that do not mention quantified variables (but warn?)
I cannot see how an empty list of tyvars is useful or desirable in practice: data Foo = Foo (forall . Int) is equivalent to just data Foo = Foo Int so why bother to permit the former? It probably indicates some error in the thinking of the programmer, so the compiler should bring it to her attention.
On the other hand, I can imagine a use for phantom type variables in the quantifier (especially if they occur in multi-parameter predicates, but not in the type). So I think accepting them with a warning is reasonable.
I can also imagine predicates that do not mention locally-quantified variables - the assumption must be that they mention variables bound on the LHS of the datatype decl instead? e.g. the Show predicate here:
data Foo a b = Foo a b | Bar (forall c . (Show b, Relation b c) => (b,c))
Hmm, maybe a simpler version of this example would illustrate what you mean by the proposal (first of the three bullets) to allow an empty quantifier list:
data Foo a b = Foo a b | Bar (forall . Show b => b)
In which case, does this even count as a polymorphic component at all? Is it not rather GADT-like instead?
data Foo a b where Foo :: a -> b -> Foo a b Bar :: Show b => b -> Foo a b
I was thinking that we should allow those special cases because I could not see a reason to disallow them (rather then having a compelling example to use them). You make a good point though, that some of them might indicate an error in the program. So, I guess, the main decision is: do we want to make them illegal (i.e., require an error) or suggest that implementations report a warning? I have no strong feelings either way, but I guess we need to pick something.
Constructor that have polymorphic components cannot appear in the program without values for their polymorphic fields.
I didn't fully understand this requirement. If Haskell-prime gets rank-2 or rank-n types, then do we need to restrict constructors in this way?
The issue is the same as for rank-2 types. My suggestion is based on the design adopted by Hugs. The basic idea is that by requiring that functions with rank-2 types (in particular, constructors that have polymorphic fields) are applied to all their polymorphic arguments, we ensure that expressions can be typed by simple types as in HM (and not type schemes). On the pragmatic side this has the benefit that the rank-2 type extension is quite easy to add to a Haskell'98 implementation: the arguments to rank-2 functions are checked pretty much in the same way as expressions with explicit type signatures. The only difference is that the type signature may contain free type variables which doesn't happen in Haskell 98. On the theoretical side we have the benefit that this fairly conservative extension to the type system (we are still working essentially in HM) gives us a big increase in expressiveness (e.g., we can encode System F programs in Haskell). The reason that the type system extension is quite simple is that Haskell 98 compares types for equality by name (as opposed to examining their structure). Other alternatives are systems like MLF (by Didier Le Botlan and Didier Rémy) and the relaxed system implemented by GHC. I think that they are both quite interesting but I must admit that for the purposes of Haskell' I am partial to the simplicity of Hug's design. The reason is that I feel that I can explain it to an ordinary Haskell programmer without too much difficulty and it has been sufficient for the situations when I've used rank-2 types. I could be unfairly biased, however, which is why discussions are most welcome! :-) -Iavor