Modular compact linear types

[skaller]

At present, a compact linear type like 7 is just a discrete set of values.

It is tempting to define addition, modulo 7, but opposed to that, an increment for iteration might be served better by a bounds check; that is: should

`6:7 + `1:7

wrap to 0, or trigger an overflow error? The current situation is simple: there is no addition so the question is moot.

It may be worth defining

\Z[7]

to be the additive cyclic group, with addition modulo 7. More generally, any compact linear product can be regarded as an additive group, and we obtain the corresponding isomorphisms with coercions on the underlying compact linear type. For example:

\Z[6] iso \Z[2 * 3] iso \Z[2] * \Z[3]

At least one case where modular arithmetic is useful is defining the determinant of a matrix as the sum of all the elements multiplied by their minors. The formula works best with modular arithmetic because it doesn't require any sign swapping crud.

Such groups can also be extended to allow multiplication by an unsigned integer, which is just repeated addition.

Even more ambitious, extension to allow multiplication and thus rings.
And on to R-modules (generalisations of vector spaces to drop the requirement
that the scalar type be a field down to just any old ring with unit).