
4 Nov
2010
4 Nov
'10
4:13 a.m.
| > The exact syntax is a problem (as usual). We have the technology now. The | question is how important it is. | | I think extending the syntax for contexts would be sufficient: | Write a ~~ b for "a can be converted to b by wrapping / unwrapping | newtypes", which is a conservative approximation of "a and b have the | same representation". | | Then we can define | | safeCoerce :: (a ~~ b) => a -> b | safeCoerce = unsafeCoerce Yes, that's right. When I said "we have the technology" I meant that we (will) have something similar to ~~. See our paper "Generative Type Abstraction and Type-level Computation" http://www.cis.upenn.edu/~sweirich/newtypes.pdf. No unsafeCoerce required. Simon