[TYPES] Parametricity with subtyping and a Top type

[Derek Dreyer]

I observed similar oddities when I tried to include a Top "signature" at 
one point in a type system for higher-order modules.

But I don't view this as breaking parametricity.  Isn't the point just 
that at Top everything is observationally indistinguishable?  So, in 
particular, \x.\y.x and \x.\y.y are in fact equivalent functions, when 
considered at the type forall a. a->a->Top, because there is no way to 
tell apart their outputs.

Derek

Tim Sweeney wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 
> Does subtyping and the existance of a Top type necessarily break
> parametricity?
> 
> Parametricity guarantees that every function of type forall a.
> a->a->Bool is a constant function.  The same derivation appears
> applicable to forall a. a->a->Top also, implying that it too must be
> constant.  But \x.\y.x and \x.\y.y are distinct functions inhabiting
> forall a. a->a->Top.
> 
> What has gone wrong here?
> 
> Pierce's thesis touches on Top in F/\ but doesn't seem to address
> parametricity.
> 
> Does there exist a systematic study of type system extensions known to
> be compatible or incompatible with parametricity?
> 
> Tim Sweeney
>