@derrickbeining asked some good questions about the Ring type class on Slack and I think they deserve a response here.
Can someone explain why
Data.Ringsupports subtraction? From the little bit of googling I’ve done, I don’t see any definitions of Rings that say anything about subtraction.
As you’ve probably found, definitions of rings don’t usually mention subtraction specifically, they usually talk about additive inverses instead. That is, there’s an function negate :: a -> a with the property that for all a, we have a + negate a = zero. Given a negate function, there is only really one sensible choice for defining subtraction: a - b would be defined as a + negate b. So I would say that subtraction is essential to rings, it’s just that this is not immediately obvious from the definition.
PureScript has opted to put it the other way around: instead of having negate be part of the definition of the class and defining sub in terms of negate, we put sub inside the class, since it’s generally the one we care more about anyway, and define negate as \a -> zero - a.
The laws given for the PureScript Ring class are then an attempt to describe the same mathematical structure, given that we are taking sub as part of the definition rather than negate. (In the process of writing this out I am coming to think it hasn’t quite been successful; I think our Ring class is a bit weaker than the real definition of a ring. However, this post is long enough already, so I’m going to continue this thought elsewhere.)
Also, the definition of the additive inverse law in the docs is described as
a - a = (zero - a) + a = zero, does this meanRingcan’t be properly implemented for unsigned integers that don’t support overflow (just throws instead)?
Correct. An unsigned integer type which doesn’t support overflow is definitely not a ring, because in a ring, every element needs to have an additive inverse such that if you add an element and its additive inverse together, you get zero.
Is the
(zero - a) + a = zerobit actually necessary? Everywhere else online I’ve seen defines the additive inverse only asa + (−a) = 0
With the approach we are taking, yes. For example: suppose I have a type in PureScript which can represent all of the nonnegative integers, with the normal Semiring instance. If we only require that a - a = zero, then I can define subtraction as, say, \x y -> if x == y then zero else x, or even as \_ _ -> zero. Both of these satisfy a - a = zero, but neither gives you a valid subtraction operation.