Skip to content

Instantly share code, notes, and snippets.

What would you like to do?

Why there can be no EuclideanRing b => EuclideanRing (a -> b) instance

One of the defining features of a EuclideanRing is that you can divide any pair of elements, as long as the divisor is nonzero. Specifically, if you have a euclidean ring R, with x, y in R, and y /= zero, we need to have x = (x / y) * y + (x `mod` y).

We do have a Ring b => Ring (a -> b) instance, where multiplication is defined as follows:

instance ringFunction :: Ring b => Ring (a -> b) where
  mul f g x = f x * g x

that is, the product of two functions f and g is a new function which applies its argument to each of f and g and returns the product of the results.

Given this, if we were going to define a EuclideanRing b => EuclideanRing (a -> b) instance, we would probably want to define div as follows:

instance euclideanRingFunction :: EuclideanRing b => EuclideanRing (a -> b) where
  div f g x = f x / g x

This, unfortunately, won't do. Suppose that we choose a function g such that there exists some x with g x = zero, but also g is not constant. The zero function in this context is constant, i.e. it is equal to \_ -> zero, and therefore g is not the zero function, or in other words, g is nonzero. Since g is nonzero, we should be able to divide by it. Now, consider the expression (f / g) x; this will be the same as f x / g x, which by assumption, is equal to f x / zero. But this is undefined, so f / g is undefined.

Essentially, if we want to define division of functions in this manner, the EuclideanRing laws say that division has to work as long as the divisor is nonzero. To divide functions, we need a much stronger guarantee than these laws can give us: namely, that zero does not appear anywhere in the image of the divisor.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.