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