[TYPES] Parametricity with subtyping and a Top type
dreyer at tti-c.org
Thu May 12 09:10:54 EDT 2005
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, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 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