Why not allow empty record updates?

[wren ng thornton]

On 11/15/11 8:07 PM, wagnerdm at seas.upenn.edu wrote:
> Quoting wren ng thornton <wren at freegeek.org>:
>> 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