[TYPES] Parametricity with subtyping and a Top type

[Haruo HOSOYA]

FYI, this subject is dicussed in the following paper.

Subtyping and Parametricity (1993)
Gordon Plotkin, Martn Abadi, Luca Cardelli

Hope this helps.

Haruo

On 2005/05/12, at 23:10, 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