unsafeCoerce and type aliases under type applications
wren ng thornton
wren at freegeek.org
Fri Dec 9 19:46:24 CET 2011
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
More information about the Libraries