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