I’m new to PS and am exploring the type classes for numbers and math stuff. I was messing around with implementing some smaller integer types like Int8 with the same classes as Int. Once I started writing property tests to verify the laws were upheld, I realized I couldn’t get the EuclideanRing laws to pass because overflow wrapping messes things up. For instance, the integral domain law is violated because bottom * 2 is zero. Also, the submultiplicative euclidean function law is violated because degree bottom is greater than degree (bottom * 2); same with top instead of bottom.
This made me we wonder if things worked differently for Int somehow, but it doesn’t. Int has the same issue. I’m wondering if I am misunderstanding something or if this is expected and just accepted due to limitations of machine integers. If it’s expected, why use this class with these laws?
Not sure if the Semiring docs answer this question:
Note: The Number and Int types are not fully law abiding members of this class hierarchy due to the potential for arithmetic overflows, and in the case of Number , the presence of NaN and Infinity values. The behaviour is unspecified in these cases.
Yes, this is expected. The way I see it, when you use Int, it is up to you to make sure that you are not dealing with values which get too close to bottom or top, because then your program likely won’t behave as it’s meant to. If you’re not doing that, then all of the instances are law-abiding. I realise that this reasoning may be a bit disappointing, and I wouldn’t accept it in most cases, but in the specific case of numbers, more or less the entire rest of the programming world uses twos-complement with a fixed number of bits for integers, and trying to be more “principled” by doing something like using arbitrary precision integers everywhere would undermine the goal of easy interop (and arbitrary precision integers have some other quite severe drawbacks, like poor performance and theoretically unbounded memory usage).
I think the class still makes sense, because it lays out boundaries for what is considered to be a sensible division operation so that it rules out a lot of less justifiable instances, and it also allows us to define useful operations like gcd and lcm. For example, you might consider defining an instance for functions which defines f / g to be \x -> f x / g x, but these laws rule that out because that instance would result in the behaviour being undefined whenever g evaluates to zero.
We should probably update the documentation to specifically mention which laws are broken by which instances. Int is a completely valid Ring, for instance (or rather it can be, we just need to switch multiplication to use Math.imul instead of *).
I think the reason I find this acceptable is that Int is intended to be an approximation of the integers, and integers are a real Euclidean ring; it’s only because of overflow that EuclideanRing Int isn’t law-abiding. Arbitrary precision integers would be able to provide a law-abiding instance… well, they could, if we changed degree to return an arbitrary precision integer. But otherwise there’s nothing stopping a law-abiding instance, and we don’t really expect degree to be used very often anyway.
I see, thanks for sharing your take. Well, so I guess the only thing I want to figure out, then, is how to write property tests for exceptions like this. Do I just filter out top and bottom from the generated inputs? Feels like cheating.
In general I would say that the goal should be to identify the boundaries of when you expect the laws to hold, and include everything else in the values you’re generating. That way, if it turns out your implementation is failing to pass law tests more often than you expect it to be, you’ll still catch it. In this case I doubt just filtering out top and bottom will be sufficient; for example, with an integer type with N bits, you’ll find that the integral domain law will be violated with any pair of powers of 2 whose exponents add up to at least N. For example 16 * 16 = 2^4 * 2^4 = 0 with Int8.
I think I would expect all of the laws to be satisfied provided that no overflows or underflows occur. So I would say that I expect a * b /= zero and that degree a <= degree (a * b) as long as a * b doesn’t over/underflow. I think the non-negative degree and quotient/remainder laws should be satisfied for everything.