On 10/18/07, Janis Voigtlaender
Yes, but that's a problem of the Arrow library writer, not of GHC. The compiler will never check a RULE.
I'm going to disagree a bit here; it's not the problem of the Arrow library writer at all, it's the problem of the implementor of the faulty arrow (me, in this case). The papers describing arrows clearly state a set of laws which arrows are expected to follow, and the RULES specify those laws clearly to anyone looking at the definition of Arrow. Also, for arrows in particular, which have hardwired compiler support, it's more difficult for a user to separate "the library" from "the compiler"; they go hand in hand.
So I can, for example, write a rule that "sum xs" is zero for any list xs.
Sure, but you're not stating a valid law for lists. Now, if on the other hand, you had: -- Invariant: the elements of a ListZero to always sum to 0 newtype Num a => ListZero a = ListZero { unListZero :: [a] } -- code to implement some useful operations on this type {-# RULES "sum/unListZero" forall as. sum (unListZero as) = fromInteger 0 #-} This rule would be valid according to the documentation specified. It's not a big step from here to specifying the laws that instances of a particular class must specify. That's what they're for, after all; a typeclass is more than just overloading.
I think what Simon was asserting is that none of the internal logic of GHC assumes any laws to hold for any type classes.
If that's the case, it doesn't address my original point at all, which was talking about the applicability of class laws to optimization RULES. Having to restate the arrow laws as optimization rules for each instance of Arrow would waste a lot of code, as well as requiring people who implement an Arrow to know not just the Arrow laws but the internals of GHC's optimization RULES system in order to get the (often very significant) benefits of the compiler being able to optimize based on those laws. -- ryan