On 12/4/11 5:17 AM, Joachim Breitner wrote:
N.B., newtypes are safe in the sense of congruent rewriting; i.e., if X is a newtype of Y, then we can rewrite X to Y (or Y to X) in any subterm of the type term (just like if X = Y or X ~ Y). It's not just at the top-level of the type term.
that is what I would expect at first glance, but at least some type features break this behavior:
Ah, yes, type families can break the behavior because they're functions at the type level, and therefore non-parametric since they can do type-case analysis on their arguments. Associated types also break the newtype congruence for the same reason, they're functions at the type level and can perform type-case analysis on their arguments and so are therefore non-parametric. The congruences I meant were for proper type constructors (i.e., the primitives like (->) and (,) as well as parametric datatypes). Since these are all parametric, they can't distinguish whether their type-arguments are newtypes or original types, and therefore they cannot change their representation based on that. It's the use of non-parametricity to change the representation which causes TF/AT to break. Other than the non-parametricity of TF/AT, the only other issue I can think of is to do with type classes. In terms of unsafeCoerce, it's sound to replace a type class' argument by a newtype (or if it's already a newtype, then replace by the original type)--- because the representations for both the instance dictionary and the values of the type are still the same. However, just because you have an instance of Foo X doesn't mean you have an instance of Foo Y, so that could mess things up if you can confuse the compiler into accepting a program which will ultimately need access to an instance that doesn't exist. And even if you have both instances, you may screw up the semantics of functions which rely on the semantics of the particular instance at hand. This is Erik Hesselink's example about coercing Map X to Map Y. Doing so is sound in the sense that the program will not crash due to corrupted memory etc. However, doing so will not preserve the semantics of the functions operating on Map, so it may not be sound in the way you would like. As always, you must be clear about whether you want to preserve the representation or the semantics, because you can't always do both. -- Live well, ~wren