[Prev][Next][Index][Thread]
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]