[TYPES] Parametricity with subtyping and a Top type
martini at cs.unibo.it
Thu May 12 23:14:10 EDT 2005
The fact that \x.\y.x and \x.\y.y are distinct normal forms
only says that you must distinguish between plain untyped beta-
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.
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
On May 11, 2005, at 19:45, Tim Sweeney wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/
> 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