This message is about scoped type variables. I'm sending it to the Haskell
mailing list, because I think that the question of scoped type variables is of
general interest to Haskellers, but I suggest that you all send *replies* to
Haskell Café, where this thread originated.
Simon
The thread was provoked by Nicholas's message about scoped type variables
http://www.haskell.org/pipermail/haskell-cafe/2006-October/018947.html
I've thought a lot about this scoped-type-variable issue, and failed to come up
with a truly satisfactory solution. As several of you have noticed, GHC 6.6
changes design wrt GHC 6.4. Perhaps it'd help if I explained what the problem
is, and then some of you may be able to figure out a better solution.
For reference
GHC 6.6:
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#scoped-type-variables
GHC 6.4:
http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html#scoped-type-variables
| I'd like to not have to introduce the forall, because with that comes
| introducing the entire context of the type. Thus I have to maintain
| any changes to the context, which I would prefer to leave to inference
| for modularity's sake.
|
| In 6.4 I was able to fix this without having to introduce the forall;
| I could introduce scoped type-variables in patterns to get the job
| done.
Well, there is something to be said for the forall approach [plan (B)] -- it is
fully explicit, and you can see exactly what the program means. One way forward
would be to allow you to abbreviate the context of the type signature (since
that is often the awkward bit) to "...", and approach you mention as "partial
type signatures".
The only other reasonable alternative that I know of is plan (A), the one taken
by earlier versions of GHC, and OCaml. As Oleg puts it:
| Which of the two occurrences of the type variable |'a| a binding one? Who
| cares... It just works: within the same expression, the same type
| variable stands for the same type.
(I think it does matter which the binding occurrence is, because Oleg's comment
begs the question "when are two type variables in the same expression?". In
earlier versions of GHC, it was precisely specified which was the binding
occurrence. However, that's a detail.) A big difference between the two
approaches is that with (B) a type variable stands for a *type variable*,
whereas in (A) it stands for a *type*.
So why did we switch from (A) to (B)? Because of type inference for GADTs. If
you read our paper "unification based type inference for GADTs" (on my home
page) you'll see that
a programmer-written type signatures always describes a rigid type
("rigid" means completely known from birth -- no nonsense about unification
etc.) It's very important for GADTs to know when a type is rigid (see the
paper).
That invariant in turn motivates the rigidity of type variables, and hence plan
(B).
Now, one could combine (A) and (B). It'd be possible to have rigid type
variables (bound by foralls) standing for type variables, and wobbly ones
(bound by patterns) standing for types. That would do what you want, but it'd
be yet more complicated, and I hesitate before making GHC's type system more
complicated.
Other alternatives would be: do something about partial type signatures; or
make GADT type inference more sophisticated (and thereby perhaps less
predicatable).
So there you have it. For myself I'm not yet convinced that plan (B) is so
bad. Maybe we should do something about partial type signatures, which might
be useful regardless of scoped type variables. But I'd welcome better
designs. It's an annoying issue because it *must* be solved (not having scoped
type variables is unacceptable); but no solution seems satisfying. However,
Haskell Prime must incorporate scoped type variables in some form!
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
