Scoped type variables

[Mark P Jones]

Hi Simon,

| When you say there's a good theoretical foundation (typed lambda
| calcului) I think you are imagining that when we say
|=20
| 	f (x::a) =3D e
|=20
| we are saying "There's a /\a as well as a \x::a in this definition".

No, that's not what I'm thinking.  When you say "f (x::a) =3D e", I'm
reading it as meaning something like: "f =3D \(x::a).e".  This is the
typed lambda-calculus perspective that I was referring to.   And, in
such systems (whether simply typed or polymorphicly typed) the type
annotation on the lambda bound variable x does not bind any type
variables appearing in a.  (And note that the type annotation may not
contain any variables, or it could contain repeated uses of the same
variable, etc...)

Binding of type variables is a separate matter.  It may be done by
some kind of /\, either explicit or implicit.  For the binding above,
those variables would have to be bound somewhere, either added,
implicitly to the binding of f, or else to some enclosing function.

| But I'm suggesting something different
|=20
| * Place the big lambdas wherever they would be now (i.e. not =
influenced
|    by the position of (x::a) type signatures.
|=20
| * Explain the pattern type signatures as let-bindings for types.  Thus
|   we might translate f to system-F like this:
|=20
| 	f =3D \x::T -> let-type a =3D T in e
|=20
| I've use let-type here, but one could equally well say (/\a -> e) T.

This is a different interpretation of type annotations than the one
you'll find in many typed lambda-calculi.  (That's a statement of
fact rather than a judgment of merits.)  In fact I'm not aware of
any work on type systems like this.  The simple translation that you
give for let-type looks ok from the perspective of System-F, say.
However, in the context of Haskell, I think it would be prudent to
determine how it extends to and interacts with things like type
inference, polymorphism, and overloading.  Perhaps it would be worth
considering a new language construct, such as:

   let-type expr :: type in expr

with the intention that the first expr is not evaluated, but used to
guide the binding of type variables in the "type" part, which would
then be in scope in the second expression.  This is a little more
powerful than your let-type because it allows a kind of pattern
matching on type expressions.  But I don't know if this would be a
well-behaved construct, or if it would be useful ...

| OK, so there are two questions
| a) does that answer the question about the techincal foundation
| b) is it a good design from a software engineering point of view
|=20
| I hope the answer to (a) is yes, but I realise that opinions may =
differ
| about (b).

I'm not persuaded about (a), I can't comment on (b), and I think there
should be a third question:

 c) when is it useful?  what holes does it fill?

All the best,
Mark

PS. Aside ... if you'd like type variables in type annotations to be
binding, then perhaps you'd also like them to work more like regular
pattern bindings and to see functions like the following:

   f              :: a -> b -> String
   f (x::a) (y::a) =3D "Yes, the arguments are the same type"
   f _      _      =3D "No, the arguments have different types"

   showList             :: [a] -> String
   showList (xs::[Char]) =3D ... show a string enclosed in "'s ...
   showList xs           =3D ... show list enclosed in [ ... ]s ...

Who needs overloading anyway? :-)