[Haskell-cafe] Class invariants/laws

[Ryan Ingram]

On 10/18/07, Janis Voigtlaender <voigt at tcs.inf.tu-dresden.de> wrote:
> 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