[TYPES] Parametricity with subtyping and a Top type
hahosoya at is.s.u-tokyo.ac.jp
Fri May 13 08:27:01 EDT 2005
FYI, this subject is dicussed in the following paper.
Subtyping and Parametricity (1993)
Gordon Plotkin, Martn Abadi, Luca Cardelli
Hope this helps.
On 2005/05/12, at 23:10, Derek Dreyer wrote:
> [The Types Forum,
> 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.
> Tim Sweeney wrote:
>> [The Types Forum,
>> Does subtyping and the existance of a Top type necessarily break
>> 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
>> 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