ModuloSemiring laws

[jonsterling]

I'm opening this ticket following a discussion with @paf31 on IRC. Here's what we've got:

-- | The `ModuloSemiring` class is for types that support addition,
-- | multiplication, division, and modulo (division remainder) operations.
-- |
-- | Instances must satisfy the following law in addition to the `Semiring`
-- | laws:
-- |
-- | - Remainder: ``a / b * b + (a `mod` b) = a``
class (Semiring a) <= ModuloSemiring a where
  div :: a -> a -> a
  mod :: a -> a -> a

This "law", however, is not valid unless we intend for the integers to fail to model the ModuloSemiring structure. In fact, the only instance of ModuloSemiring that actually follows this law presently is Unit. The problem is that nowhere has the behavior of division by zero been accounted for....

counterexample

Here's an example of where the law fails for Number. Fix a : Number, and let b be 0. Then, we have the following chain of equations:

1. (a / 0) * 0 + mod a 0
2. ==> Infinity * 0 + mod a 0
3. ==> 0 + 0
4. ==> 0

Therefore, a must be 0 for any a, which is clearly false.

discussion

what should we do? Unless I've made a mistake, this law is definitely wrong / not the intended definition of a ModuloSemiring. Can we fix it though? One option would be to say that it must only hold for non-zero b, but is that something we want to say in the type class itself? I'm curious what people think.

@garyb @paf31

[paf31]

EuclideanDomain seems like the right abstraction (although I'd also be fine with just removing ModuloSemiring honestly and putting div in DivisionRing). I would have EuclideanDomain and DivisionRing be unrelated in the hierarchy.

-- | Law: `a /= 0` and `b /= 0` implies `ab /= 0`
class Ring a <= IntegralDomain a

-- | Law: `a = b * dm.div + dm.mod` where `dm = divMod a b` and `degree dm.mod < degree b`
class IntegralDomain a <= EuclideanDomain a where
  degree :: a -> Int
  divMod :: a -> a -> { div :: a, mod :: a }

EuclideanDomain would be useful if we wanted to handle things like Gaussian integers or polynomial rings, but such things probably don't need to influence the Prelude.

[jonsterling]

@paf31 I think I like the idea of putting div in DivisionRing and separately, adding EuclideanDomain.

[paf31]

This is also the sort of thing we should figure out before 1.0, probably.

[paf31]

The EuclideanDomain approach would mean we'd have two unrelated div functions. I'm fine with that personally, but it might be a bit confusing for beginners.

Edit: beginners would probably not use EuclideanDomain anyway.

[jonsterling]

@paf31 My personal thinking is that divMod looks obscure enough that nobody will think to use it unless they "really" need it...

[garyb]

@jdegoes may have some thoughts on this too.

Removing ModuloSemiring is fine by me, in that we just made it up anyway, whereas the other divisions have some historical backing.

I wonder if it would be odd to beginners that they can't divide integers at all? Maybe less odd than allowing it though, actually 😄

[garyb]

(I'm assuming EuclideanDomain would not be in the Prelude? How about IntegralDomain?)

[jonsterling]

@garyb not sure I follow about beginners not being able to divide integers, since isn't that what divMod would do? For what it's worth, I've found it confusing in the past to have to perform two separate operations to divide integers and then figure out the remainder.

[hdgarrood]

How would we implement degree for EuclideanDomain Int? Also, could this be a problem - from wikipedia:

in general, a Euclidean domain will admit many different Euclidean functions.

(apparently a Euclidean function is another name for a degree function).

[paf31]

I'm suggesting that div would move into DivisionRing, and EuclideanDomain would be a completely different thing, a subclass of Ring and IntegralDomain, possibly in another module. The two notions of division would be unrelated.

[jdegoes]

This is a valid point, but note the laws for DivisionRing also fail for a similar reason.

I'd say that (a) there's clearly something between Semiring and DivisionRing (EuclideanDomain?) and that thing can have useful laws; and (2) laws for whatever that thing is called, as well as DivisionRing, probably need to explicitly exclude division by zero (someone should verify that's actually sufficient and that it's not necessary to support multiple "zeros" to define useful instances for non-numbers).

[hdgarrood]

I like being able to get both pieces of information from divMod at the same time. I also quite like having a div that works on integers, though; I find that I don't always want the mod. Is there any way to have a class with a member div :: a -> a -> a and sensible laws, such that, for Int, div = _.div <<< divMod?

Also I think we really ought to have some way of dividing integers in the Prelude. What reason is there not to include EuclideanDomain in the Prelude?

[paf31]

I don't think EuclideanDomain is between Ring and DivisionRing since Number is a Ring and a DivisionRing, but not a EuclideanDomain as far as I know. I think it is its own branch of the hierarchy with Ring a <= IntegralDomain a <= EuclideanDomain a.

Edit, or perhaps the reals are a euclidean domain, where the degree is just a constant? In which case inserting EuclideanDomain there possibly does make sense.

[hdgarrood]

Ok then - if we can have both EuclideanDomain Int and EuclideanDomain Number, can we also have div = _.div <<< divMod, and mod = _.mod <<< divMod, which would then work on both?

[garyb]

Int is still a DivisionRing like it always was.

Now I'm confused 😄... Int isn't a DivisionRing now, and I don't see how it could be, since it doesn't meet the laws.