{{ message }}

Instantly share code, notes, and snippets.

# hdgarrood/euclidean-ring-function.md

Last active Aug 18, 2017

# 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.