Let me just begin by sharing my experience with scoped type variables. I've
found them very useful in a project were I was to generalize a substantial
code base. Many of the functions had local definitions whose type were
simply not expressible without scoped type variables. During this work I
found an interesting interplay between multi parameter type classes and
scoped type variables. An example would look something like this:
f :: C a b c = a - b
f a =
let g = ...
The important thing to note is that the type variable c in f's signature
occurs neither in the argument nor the result type of f. Hence c is not
bindable by lexically scoped type variables. But suppose c is part of g's
type. Then we still have no way of expressing g's type! This thing has
bitten me and so I welcome the change you're planning.
As for your questions I would prefer 1b although I don't think it is a big
deal. For your second question I would go for 2c (which you've called 2b :).
That's because I don't use result type signatures. Other people will surely
disagree.
Cheers,
/Josef
-Original Message-
From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On
Behalf Of Simon Peyton-Jones
Sent: den 25 november 2004 11:44
To: [EMAIL PROTECTED]
Subject: [Haskell] Lexically scoped type variables
| This is a great example, thanks for posting it. However, I feel like
| the real problem in this example is the lexically-scoped type
| variables declared with your function f.
Paul's message gives me an excuse to consult the Haskell list about the
design of lexically scoped type variables. I have a two particular
questions I'd like your advice about. (This is nothing to do with
monomorphism restriction, or Lennart's original puzzle.)
I'm sending this message to the main Haskell list, to maximise
readership, but I suggest that
you reply to [EMAIL PROTECTED]
Thereby to avoid spamming the main Haskell list, which is meant to be
low-bandwidth. I believe I've set the reply-to field of this message to
achieve this goal. [Perhaps others can do the same?!]
Simon
Background
First, for background you might want to glance at Lexically scoped type
variables, an unpublished paper available at
http://research.microsoft.com/%7Esimonpj/papers/scoped-tyvars
I don't want to take time in this message to discuss why we want scoped
type variables; I'll just take it for granted here.
One design choice discussed in the paper, and implemented in GHC, is
that we can bring new lexically-scoped type variables into scope by
mentioning them in a pattern type signature:
f (x::a) =
Here 'a' is a name for the type of x, and 'a' scopes over f's body, and
can be mentioned in type signatures in f's body. Sometimes one wants to
name types in the result* of f, rather than it its *arguments*. For
example
head (xs::[a]) :: a = ...
Here, the :: a before the = gives the type of head's result. If a
result type signature binds a type variable, that type variable scopes
over the right hand side of the definition.
In GHC, it's not necessary for the type that 'a' names to be a type
variable; it could be Int, for example:
f (x::a) = x + (1::Int)
Already this embodies several design choices. For example, we know that
'a' is a *binding* for 'a' because there is no 'a' already in scope,
otherwise it'd be an *occurrence* of 'a'. (An alternative would be to
mark binding sites somehow.) Also once could require that 'a' names a
type variable rather than an arbitrary type. But for this message I
want to take GHC's design as given.
QUESTION 1 -
In GHC at present, a separate type signature introduces no scoping. For
example:
f :: forall a. a - a
f x = (x::a)
would be rejected, because the type signature for 'f' does not make
anything scope over the right-hand side, so (x::a) means (x::forall
a.a), which is ill typed.
An obvious alternative, taken up by (among others) Mondrian and
Chamaeleon, is to say that
the top-level quantified variables of a separate type signature
scope over the right hand side of the binding
In the above example, then, the 'a' bound by the 'forall' would scope
over the right hand side of 'f'.
I've argued against this in the past, because the construct (forall a.
type) patently scopes 'a' only over type. But my resolve is
weakening. It's just too convenient! Furthermore, it binds a *rigid*
type variable (i.e. 'a' really must name a type variable) and that's
important for GADTs... which strengthens the case.
In short, I'm considering adopting the Mondrian/Chameleon rule for GHC.
There are two variations
1a) In the example, 'a' is only brought into scope in the
right hand side if there's an explicit 'forall' written by
the programmer
1b) It's brought into scope even if the forall is implicit; e.g.
f :: a - a
f x =
