[TYPES] Parametricity with subtyping and a Top type

[Simone Martini]

The fact that \x.\y.x and \x.\y.y are distinct normal forms
only says that you must distinguish between plain untyped beta- 
conversion and
and a notion of equality between terms, that has to be relativized
with respect to a type. These two terms are thus equal in
forall a. a->a->Top, but different in forall a. a->a->a.

We studied some of the phenomena arising with subtyping
and a Top type in the context of parametricity in
    Luca Cardelli, Simone Martini, John C. Mitchell, and Andre Scedrov.
    An extension of System F with subtyping
    Information and Computation vol. 109(1994), 4--56.

-s.
---------------------------------------------------
Simone Martini                          tel: +39 051 2094979
Universita' di Bologna                  fax: +39 051 2094510
Dip. di Scienze dell'Informazione
Mura Anteo Zamboni, 7
40127 Bologna BO                        www.cs.unibo.it/~martini
Italy

On May 11, 2005, at 19:45, 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
>