# 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