idris-hackers/idris-algebra

This is an attempt at painting as many bikesheds as possible with a typeclass hierarchy for idris reflecting "Algebra"

idris-algebra's Issues

Implementing ring-like and multiple operator algebra structure.

Haskell's algebra makes group-like algebra of both additve and multiplicative, which I think is way too verbose.
It looks named implementations is better for implementing two different operators belong to the same structure. Any though on this?

Definition of quasigroup is wrong

The definition of quasigroup posed says that a quasigroup can be determined by a type a, a binary operation op : a -> a -> a and two unary operations rinverse, linverse : a -> a.

Supposing op refers to the operation of a quasigroup on a, and rinverse, linverse refer to left and right division, the definition is wrong - for fixed y, there is no single y' : a such that (x : a) -> (x y) y' = x.

Now, suppose each x : a is identified with the left translation permutation L(y) : r ↦ yr of some y in b where b is a quasigroup in the sense above. Then although L(y) determines the inverse permutation of L(y), to say that op is composition of permutations and each L(y) such that y is in b is given by some inhabitant of a is, assuming a is the least such type closed under op as the type of op implies, to say that a = LMlt(b). But LMlt(b) does not determine b -- in fact, for most 5-element loops b, LMlt(b) contains every permutation on 5 elements, and therefore without knowing naming scheme of LMlt(b) elements relative to elements of b (the map b → LMlt(b), x ↦ L(x)), b cannot be determined up to isomorphism from the elements of LMlt(b), and moreover more than one isomorphism class of b of order 5 has the property that it is possible to express the left permutations of each 5-element loop up to isomorphism as elements of a = LMlt(b). Therefore knowing a, op, linverse, rinverse is not enough to know b and therefore not enough data to define a quasigroup under the proposed assumptions.

These are the two obvious candidates for a collection of natural data to determine quasigroups from first principals. Note also that a left quasigroup (one with left division, as in x (x \ y) = y) is not necessarily a right quasigroup. So the three binary operations and the equations relating them are a minimal definition.

I suggest qunder for (\) and qover for (/), since over is associated with lenses.