# Re: F-bounded polymorphism

> Satish:
> The main rule Kim suggested seems to be the right one based on
> "argument from first principles" :
>
> > Kim:
> >
> > 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.

Yeah, never reply to e-mail too quickly!  The statement above on the set
not being downward closed is true but irrelevant.

> 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

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.

The obvious proof fails, since from C + {t <: \tau'} |- t <: \tau
I can only show that C |- \tau' <: \tau[\tau'/t] (by replacing t by \tau'
everywhere in the first proof).  Does anyone have a proof that the two
statements in the hypotheses are equivalent or have an example in which
C + {t <: \tau'} |- t <: \tau
but not C + {t <: \tau'} |- tau' <: \tau.

(Remember the complicating factor is that both \tau and \tau' may involve t!)

Kim Bruce