[TYPES] Parametricity with subtyping and a Top type

[Matt Hellige]

[Derek Dreyer <dreyer at tti-c.org>]
> [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.

Yes, I'd argue that it's the implied presence of down-casting which
causes the problem in this case... But of course if we assume an
OO-style of dynamic method dispatch (or virtual methods, or whatever),
that mechanism acts in effect as a sort of "safe downcast," and would
also have to be disallowed.

Matt

-- 
Matt Hellige                  matt at immute.net