On 11/15/11 8:07 PM, wagnerdm@seas.upenn.edu wrote:

Quoting wren ng thornton :

...

So far I've just defined helper functions to adjust the phantom type[1], each of which is implemented by (\x -> x { foo = foo x }). It's a horrible hack, but at least it's hidden away in library functions instead of something I have to look at. The annoying part

(a bit tongue-in-cheek, and hence not sent to the mailing list)

Forwarding to the list, because I actually have a serious response :)

As long as we're writing hacks, why not use unsafeCoerce? ;-)

In this particular case I don't care too much about representation sharing (though I do share Ed's concern), and I generally do my best to avoid unsafeFoo just so I can minimize my personal proof obligations / maximize the utility of the compiler's type checking. Though, yes, in other projects with similar considerations I've also gone the unsafeCoerce route. Other than invalidating type system guarantees, it does have the side effect that it can interfere with rewrite rules firing (since the coercion remains in the System Fc core). And the times when I really care about representation sharing are often also the times I really care about rewrite rules firing. Which in turn means I tend to add additional rewrite rules to push the unsafeCoerce around in order to get it out of the way so that other rules can fire. But I see no way of specifying these additional rules in full generality while retaining correctness--- without some additional mechanism to say things like "this newtype wrapper is opaque in these contexts (to preserve the abstract semantics), but is translucent in these other contexts (to abide by categorical laws like functorality). It's really unfortunate that these complementary goals of sharing representation and doing rewrites/fusion are at odds in current Haskell. I run into similar issues with needing to work around coercions in Coq, since they impede the evaluator and proofs of value equality due to the weakness of Coq's case analysis. That the issue shows up in Coq as well seems to imply that the root of the problem is something deeper than noone having implemented the convenience. Agda has a stronger case analysis and so doesn't run into quite the same issues, though I'm not entirely clear on the exact ways in which Agda's case analysis gains that extra power, so it's unclear whether we could (meaningfully) add the power to Haskell without going whole hog into dependent types. Of course, this all is related to the problem of strong updates; it just happens that the update is Curry-identical, yet Church-different. Given the general preference for Church-style lambda calculi, it's not surprising that this exact problem hasn't been tackled (to my knowledge). Another place this problem has come up for me is in wanting to ensure representation sharing for values constructed by data constructors which don't make use of their type parameters. A trivial example would be sharing the representation of Nothing between all the Maybe types, or sharing the empty list among all the list types. That example isn't especially motivating, but there are other cases where we can end up with a large structure for which the type parameters are 'phantom' even though they may not be phantom in general (because other data constructors make use of them). That we want type updates for records with phantom types is just a symptom of the larger issue of wanting type updates for all quasiphantom/pseudophantom types. -- Live well, ~wren