Menu
In the GHC documentation for the ScopedTypeVariables extension, the overview states the following as a design principle:
A scoped type variable stands for a type variable, and not for a type. (This is a change from GHC’s earlier design.)
I know the general purpose of the scoped type variables extension, but I don't know the implications of the distinction made here between standing for type variables and standing for types. What is the significance of the difference, from the perspective of users of the language?
The comment above alludes to two designs which approached this decision differently and made different tradeoffs. What was the alternative design, and how does it compare to the one currently implemented?
545
tl;dr: The documentation says what it says because the old implementation of scoped typed variables in GHC was different, and the new documentation (over)emphasizes the contrast between the old behavior and the new behavior. In fact, the scoped typed variables you use with the ScopedTypeVariables extension in place are just plain old (rigid) type variables, and these are the same type variables you've been using in regular Haskell type signatures without scoping (even if you didn't realize they were "rigid"). It's true that scoped type variables don't simply "stand for types", but regular unscoped type variables don't simply "stand for types", either.
Longer answer:
First, setting aside the issue of scoped type variables, consider the following:
pluralize :: [a] -> [a]
pluralize x = x ++ "s"
If a, as a type variable, simply "stood for a type", this would be fine. GHC would determine that a stood for the type Char, and the resulting signature [Char] -> [Char] would be determined to be the correct type of pluralize, so there'd be no problem. In fact, if we were inferring the type of:
pluralize x = x ++ "s"
in a plain old Hindley-Milner (HM) type system, this is probably exactly what would happen. As an intermediate step while typing the (++) application, the type checker would assign x the type [a] for a "fresh" HM type variable a, and it would assign pluralize the type [a] -> [a] before unifying [a] with the type of "s" :: [Char] to unify a and Char.
Instead, this is rejected by the GHC type checker because a in this type signature is not an HM-style type variable and so does not simply stand for a type. Instead, it is a rigid (i.e., user-specified) Haskell type variable, and the type checker doesn't permit such a variable to unify with anything other than itself while defining pluralize.
Similarly, the following is rejected:
pairlist :: a -> b -> [a]
pairlist x y = [x,y]
even though, if a and b just stood for types, this would be fine (as it works for any a and b of kind * provided only that a and b are the same type). Instead, it is rejected by the type checker because two rigid Haskell type variables a and b can't unify.
Now, you might try to make the case that the issue is not that type variables are "rigid" and can't unify with concrete types (like Char) or with each other, but rather that there is an implicit quantification in Haskell type signatures, so that the signature for pluralize is actually:
pluralize :: forall a . [a] -> [a]
and so when a is determined to "stand for" Char, it is the contradiction with this forall a quantification that triggers the error. The problem with this argument is that both explanations are actually more or less equivalent. It is because Haskell type variables are rigid (i.e., because type signatures in Haskell are implicitly universally quantified) that the types cannot unify (i.e., that the unification contradicts the quantification). However, it turns out that the "rigid type variables" explanation is closer to what's actually happening in the GHC type checker than the "implicit quantification" explanation. That's why the error messages generated by the above definitions refer to inability to match rigid type variables rather than to contradictions with universal type variable quantifications.
Now, let's turn back to the question of scoped type variables. In the olden days, GHC's -fscoped-type-variables extension was implemented quite differently. In particular, for pattern type signatures, you were permitted to write things like the following (taken from the documentation for GHC 6.0):
f :: [Int] -> Int -> Int
f (xs::[a]) (y::a) = (head xs + y) :: a
and the documentation went on to say:
The pattern type signatures on the left hand side of
fexpress the fact thatxsmust be a list of things of some typea; and thatymust have this same type. The type signature on the expression(head xs)[sic] specifies that this expression must have the same typea. There is no requirement that the type named by "a" is in fact a type variable. Indeed, in this case, the type named by "a" isInt. (This is a slight liberalisation from the original rather complex rules, which specified that a pattern-bound type variable should be universally quantified.)
It went on to give some additional examples of use of scoped type variables, such as:
g (x::a) (y::b) = [x,y] -- a unifies with b
k (x::a) True = ... -- a unifies with Int
k (x::Int) False = ...
In 2006, Simon Peyton-Jones made a big commit (ac10f840) to add impredicativity to the type system which also ended up substantially changing the implementation of lexically scoped type variables. The commit text contains a detailed explanation of the change including the requirements for the new design.
A key design choice was that lexically scoped type variables now named rigid (i.e., user-specified polymorphic) Haskell type variables, rather than being more like the HM-style variables that simply stood for a type and were subject to unification.
That made the above examples (f, g, and k) illegal, because scoped type variables in pattern matches now behaved more like regular rigid type variables.
Soooo... the old design was probably a weird hack that made scoped type variables more like HM type variables and so quite different from "normal" Haskell type variables, and the new system brought them more into line with how unscoped type variables behaved.
However, complicating things further, @duplode's link in the comments references a proposal to partially "undo" this "restriction" in the context of signatures in pattern matches. I think it would be fair to say that the old design, which treated scoped type variables more like a special case, was inferior to the new design which better unified the treatment of scoped and unscoped type variables, and there is no desire to go back to the old implementation. However, the new, simpler implementation had the side effect of being unnecessarily restrictive for pattern signatures which perhaps ought to be treated as a special case where non-rigid type variables are permitted.
192
I'm adding this answer (to my own question) in order to expand on duplode's reference in the comments. ScopedTypeVariables is currently being changed to allow scoped type variables to stand for types instead of only type variables. The discussion for this change the motivation for the new and old designs. This does not, however, address the even earlier design mentioned in the question and in K. A. Buhr's answer.
In the current state, before the forthcoming change, the definition
prefix :: a -> [[a]] -> [[a]]
prefix (x :: b) yss = map xcons yss
where xcons ys = x : ys
is valid (with ScopedTypeVariables), in which b is a newly introduced type variable that stands for the same thing as a. On the other hand, if prefix is specialized to
prefix :: Int -> [[Int]] -> [[Int]]
prefix (x :: b) yss = map xcons yss
where xcons ys = x : ys
then the program is rejected: b is forbidden from standing for Int since Int is not a type variable. Simon Peyton Jones remarked on why it was designed so that b could not stand for Int:
At the time I was worried that it'd be confusing to have a type variable that was just an alias for Int; that is not a type variable at all. But in these days of GADTs and type equalities we are all used to that. We'd make a different choice today.
In the current consensus of the GHC maintainers, the limitation against b standing for Int is viewed as unnatural, especially in light of the possibility of type equalities (a ~ Int) => .... The presence of such constraints blur the lines of what being "bound to a type variable" really means. Should the examples
f1 :: (a ~ Int) => Maybe a -> Int
f1 (Just (x :: b)) = ...
f2 :: (a ~ Int) => Maybe Int -> Int
f2 (Just (x :: a)) = ...
be permitted? Under the new proposal, all four examples above are allowed.
In my own view, the tension ultimately comes from the coexistence of two very different type annotation systems. One of them has the effect of preventing you from giving different names to the same type (for instance, you cannot write (\x -> x) :: a -> b or (\x -> x) :: Int -> b and expect b to be unified with a or Int). The other enables and encourages you to give new names to things (pattern type signatures like foo (x :: b) = ...), a feature which exists to enable you to name types that would otherwise be un-nameable. The leftover question is whether pattern type signatures should allow you to alias types that are already nameable. The answer at its core depends on which of the two precedents you find more compelling.
References:
23
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With