[Prev][Next][Index][Thread]
Re: F-bounded polymorphism
I should really let Dinesh Katiyar speak for himself here but let me
just respond based on his note to the F-bounded poly workshop.
I wrote:
>
> > 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')
> > >
> ...
>
> > 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')
> >
Kim responded, in part:
>
> It appears that Katiyar's rule may be weaker than the one I proposed
> since if C + {t <: \tau'} |- tau' <: \tau then by transitivity, one can
> show that C + {t <: \tau'} |- t <: \tau. But I don't see how to prove the
> other direction.
My response again:
The other way doesn't work, but Katiyar argues that it fails only in
the case of trivial (and pathological?) examples like
C |- \forall t<:t.T <: \forall t<:U.T
which follows from the rule Kim suggested but not from the one Katiyar
favors. In particular the bound on the subtype side must be of the
form t<:t for the difference between the rules to be manifested. The
argument is a simple one based on the the cases for subtyping
judgements with a type variable on the LHS in the Curien-Ghelli
subtyping algorithm.
I don't recall if the latter is complete in any sense though.
Satish