Re: Break `abs` into two aspects

On Tue, 28 Jan 2020, Dannyu NDos wrote:

`abs` represents a norm, but its type is wrong

There are two useful meanings of `abs`, which coincide for integers. One is a norm. Another one is to define `abs` as a mapping from a ring R to a factor ring R / U(R), where U(R) is a ring of units, and `signum` as a mapping from R to U(R) such that `abs a * signum a = a`.

This enables us to implement rings (Num) and fields (Fractional) without concerning about norms. For example, Gaussian integers.

For Gaussian integers I find convenient to define `signum z` with a codomain {1, i, -1, -I} (basically, to which quadrant does z belong?) and `abs z` with the first quadrant as a codomain. Best regards, Andrew