Ring laws are too weak

[hdgarrood]

Previously: #24. At the moment, our Ring class has just one law in addition to the Semiring laws:

• Additive inverse: a - a = (zero - a) + a = zero

A mathematician would describe rings as semirings which have the following additional structure:

• A function negate :: a -> a,
• with the property that a + negate a = zero,

and would then define a - b as a + negate b. It's easy enough to see that our law can be derived from the mathematical definition of a ring. However, we can't go in the other direction, because our Ring law only talks about the behaviour of sub when applied to two identical values, or when applied to zero and something else, which means that sub is free to do something nonsensical in other cases, which means that there are types which admit law-abiding Ring instances but are not actually rings. Here's a gist with the smallest example I could think of:

• https://gist.github.com/hdgarrood/9a9906f35f13d02ee39d6e85c811ff8c
• Or view it on Try PureScript: https://try.purescript.org/?gist=9a9906f35f13d02ee39d6e85c811ff8c

I think we can fix it by changing the laws to this:

• Additive inverses: a - a = zero
• Compatibility of sub and negate: a - b = a + (zero - b)

Note that we don't actually need two equations for the additive inverses law because we already know that addition is commutative from Semiring.

We can derive the current laws from the above ones very easily. We already have a - a = zero. As for the other part:

(zero - a) + a
= a + (zero - a) # addition is commutative
= a - a # compatibility law
= zero # inverses law

So the suggested laws are at least as strong as the current ones. What we really want to prove, though, is that the suggested new laws give us something which is actually equivalent to a ring. Of course, a + negate a = zero is immediate, but then again that was also immediate with the previous definition. So what's the difference? Well, the mathematical approach has defined what a - b should evaluate to for all pairs a, b. We need to ensure that we do the same; that's what the compatibility law does.

The gist also contains a test showing that the compatibility law correctly prevents the example I used before from being a law-abiding Ring.