Re-add DivisionRing?

[hdgarrood]

I am working on a quaternion library and I was wondering if it might make sense to add a DivisionRing type class again, as follows:

class Ring a <= DivisionRing a where
  recip :: a -> a

with the law that x * recip x = recip x * x = one for all nonzero x. There's no requirement for the ring to be commutative, and so this would allow us to provide a DivisionRing Quaternion instance.

If we were going to do this, we should change Field so that DivisionRing is a subclass as well.

Now of course with any EuclideanRing you can simply write one / x for recip x. Also, admittedly, the only 'useful' instance I can think of is Quaternion; I did some googling and wasn't really able to find any other useful examples of non-commutative division rings. But I think it would be nice to have a way of asking for the multiplicative inverse of an element of an arbitrary division ring without requiring it to be commutative.

[paf31]

Do you remember why it was removed?

[garyb]

In the previous discussion you dropped it from the proposed hierarchy: #61 (comment) 😉

[paf31]

From the previous issue for anyone wondering:

Quaternion would be a EuclideanDomain but not a CommutativeRing in this setting, but we wouldn't capture the fact that it had multiplicative inverses. This suggests that it makes sense to keep EuclideanDomain <= DivisionRing and have (CommutativeRing, DivisionRing) <= Field. Then Quaternion would be a DivisionRing but not a Field.

I'd be fine with adding that class, with the additional law that one / x = recip x for any Field, since that's where div and recip join up.

[hdgarrood]

I'm not sure that that additional law would be necessary, I think it's implied by the existing EuclideanRing and Field laws.

[hdgarrood]

That is: let x be a nonzero value of some type A with a Field instance (under the proposed hierarchy). We have from the Field laws that one `mod` x = zero, and so combining this with the EuclideanRing laws we see that if we define q = one / x then we have that one = q * x. Now, the DivisionRing law saying that recip x * x = x * recip x = one establishes that the nonzero values of the type A form a group under multiplication, and of course group inverses are unique, so we must have q = one / x = recip x.

[paf31]

Is there any reason to formulate DivisionRing in terms of reciprocals instead of division?

[paf31]

Also, if we have two division operations, is it going to be clear which one users should use when they want to work abstractly?

[hdgarrood]

How would you formulate DivisionRing in terms of division? With noncommutative rings you can have left and right division, ie p * recip q or recip q * p, which might have different results. I think it's a bit of a misnomer really but that is what it's called; in my mind it's a ring for which the nonzero elements form a group under multiplication, so this was the natural formulation.

[hdgarrood]

Come to think of it, if we were to add DivisionRing like this, then a Field is precisely a commutative division ring, so the Field class would arguably become redundant.

[hdgarrood]

In fact, if we did this, would it make sense to have:

class (CommutativeRing a, DivisionRing a) <= Field a
instance field :: (DivisionRing a, CommutativeRing a) => Field a

so that people could still write functions with Field constraints for the sake of brevity and familiarity, but people wouldn't need to declare their own Field instances?

[garyb]

Unfortunately instances like that don't work, they overlap with everything as the a commits before the constraints are checked.

[hdgarrood]

Yes, my idea was that that instance should overlap with everything because nobody should be declaring Field instances themselves, rather declaring DivisionRing and CommutativeRing instances and letting the compiler figure out that it's a Field.

[garyb]

Oh, I see! That's an interesting way of doing it.

[hdgarrood]

Also I imagine the following might come in useful at some point in the discussion:

Suppose a type A has a valid DivisionRing instance. If it also has a EuclideanRing instance, this instance must be equivalent to the following to be law-abiding:

instance EuclideanRing a where
  div a b = a * recip b
  -- actually any nonnegative integer constant works here,
  -- but let's just stick with 1.
  degree _ = 1
  mod _ _ = zero

Proof. This follows from the submultiplicativity law on the EuclideanRing class:

• For all nonzero a and b, we have degree a <= degree (a * b)

Suppose a : A and a is nonzero. Then, degree (one : A) <= degree (one * a) = degree a. Also, degree a <= degree (a * recip a) = degree one. So degree a = degree one, i.e. degree must be constant.

Since degree is constant, we cannot possibly have degree r < degree b for any r, b : A. Therefore, for any a, b : A, with b nonzero, the quotient/remainder law tells us that a `mod` b = zero. Looking again at the same law and using this new fact, we have that a = q * b i.e. a = (a / b) * b. If we multiply both sides by recip b we see that a * recip b = (a / b) * b * recip b = a / b.

[hdgarrood]

Also, if we have two division operations, is it going to be clear which one users should use when they want to work abstractly?

So coming back to this, I guess the division operations would be:

• div :: EuclideanRing a => a -> a -> a: requires commutativity, doesn't require nonzero elements to have multiplicative inverses
• leftDiv, rightDiv :: DivisionRing a => a -> a -> a, doesn't require commutativity, does require all nonzero elements to have a multiplicative inverse.

leftDiv would be defined as leftDiv p q = recip q * p, and rightDiv as rightDiv p q = p * recip q. These functions are probably not important enough to deserve an operator, I think.

Note that

• neither set is more general than the other
• if a type supports both sets then all the functions must be equivalent
• pretty much every useful Ring instance is commutative
• Quaternion is probably the only noncommutative division ring which might end up being used in PureScript code

Given all this, I'd say that it's not a problem that there is more than one division operator, and that people should always use div if they're working abstractly unless they know they want their code to work with Quaternion (or some other noncommutative DivisionRing).

In fact, it might even make sense not to provide leftDiv or rightDiv in terms of DivisionRing but instead continue providing specialised versions in the quaternions library. However I am leaning towards providing them, because they can be expressed using only operations from this proposed DivisionRing class, and the more general type signature gives you more information about what the function can (or rather can't) do.

aside: to make sure I have leftDiv and rightDiv the right way around I checked the documentation for x \ y in Octave and also the Wikipedia page for "division". They're currently the wrong way around in my quaternions library, oops.