[Prev][Next][Index][Thread]
Re: F-bounded polymorphism
The main rule Kim suggested seems to be the right one based on
"argument from first principles" :
>
> C + {t <: \tau'} |- t <: \tau, C + {t <: \tau'} |- \sigma <: \sigma'
> -----------------------------------------------------------------
> C |- (\forall t <: \tau. \sigma) <: (\forall t <: \tau'. \sigma')
>
I must admit I did not understand the comment
> 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.
Surely, C |- \tau' <: \tau is *sufficient*, since it only requires
transitivity to conclude from this and C |- t <: \tau' that C |- t <: \tau.
The point seems to be that it may be too strong, in particular because
it does not allow use of the assumption t <: \tau'. In fact, Katiyar
has argued in favor of the slightly different rule
C + {t <: \tau'} |- tau' <: \tau, C + {t <: \tau'} |- \sigma <: \sigma'
-------------------------------------------------------------------------
C |- (\forall t <: \tau. \sigma) <: (\forall t <: \tau'. \sigma')
which is just the standard rule for bounded poly with the additional
assumption. An example of where the assumption makes a difference
(again due to Katiyar) is:
C |- \forall t<:a->(a->t).T <: \forall t<:a->t.T
Satish