[TYPES] Parametricity with subtyping and a Top type

[Martin Abadi]

You might be interested in the paper "Subtyping and Parametricity", by 
Plotkin, Cardelli, and myself, in the Proceedings of the Ninth Annual 
IEEE Symposium on Logic in Computer Science (1994).  -Martin

Derek Dreyer wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 
> 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
>>