[TYPES] Parametricity with subtyping and a Top type

Martin Abadi abadi at soe.ucsc.edu
Thu May 12 14:08:57 EDT 2005

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

More information about the Types-list mailing list