Re: F-bounded polymorphism

To: kim@cs.williams.edu, types@dcs.gla.ac.uk
Subject: Re: F-bounded polymorphism
From: Satish Thatte <satish@sun.mcs.clarkson.edu>
Date: Fri, 29 Jan 93 11:27:11 EST
Approved: types@dcs.gla.ac.uk


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')
> 

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.
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

Satish