Skip to content

Instantly share code, notes, and snippets.

@hdgarrood
Last active August 18, 2017 13:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save hdgarrood/2aa65073acf7fbdd9736780d552a8ad4 to your computer and use it in GitHub Desktop.
Save hdgarrood/2aa65073acf7fbdd9736780d552a8ad4 to your computer and use it in GitHub Desktop.

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