Instantly share code, notes, and snippets.

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

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