Re: F-bounded polymorphism

To: types@dcs.gla.ac.uk, satish@sun.mcs.clarkson.edu
Subject: Re: F-bounded polymorphism
From: kim@cs.williams.edu (Kim Bruce)
Date: Fri, 29 Jan 93 17:19:12 EST
Approved: types@dcs.gla.ac.uk
> 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