Re: F-bounded polymorphism

Phil Wadler and I wrote down the obvious rules at this year's POPL
conference and they seemed to work fine.  Phil kept notes (I didn't).
Hopefully he can correct me if I blow it.  As I recall the only rule
that took any real care was the subtyping rule for types of the form
\forall t <: \tau(t).\sigma.

I believe the correct rule for this case is as follows, where C is a
collection of simple type constraints (i.e., terms of the form t <:
\tau, for t a type variable):

C + {t <: \tau'} |- t <: \tau,  C + {t <: \tau'} |- \sigma <: \sigma'
 C |- (\forall t <: \tau. \sigma) <: (\forall t <: \tau'. \sigma')

In the above, <: should be "less than or equals" (limitations of
e-mail!), and you need the usual restrictions on occurrences of t in
C.  The only real difference from the usual bounded polymorphic types
is that one must be slightly more careful with restrictions on \tau
and \tau' since t may occur free in \tau and \tau'.  In the simpler
calculus, you just needed to show C |- \tau' <: \tau.  Here you need
the more complex rule since the set of values for t which satisfy
t <: \tau need not be downward closed.

For this to go through one must also slightly loosen up the
constraints on C, in that a simple type constraint, t < \tau, can be
added to C as long as t does not occur free in C.  (I haven't checked
all of the consequences of this, but it doesn't seem like a problem -
I needed to do similar, though weaker loosenings of the definition of
C for my paper in this year's POPL proceedings).

	Kim Bruce

[The rule above matches my notes of the conversation with Kim.  -- Phil]