unsafeCoerce and type aliases under type applications

[wren ng thornton]

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