or Addition

For practical reasons, we begin the class tree with Additive. Starting with Associative and Unital, or using Semigroup and Monoid from base tends to confuse the interface once you start having to disinguish between (say) monoidal addition and monoidal multiplication.

zero + a == a
a + zero == a
(a + b) + c == a + (b + c)
a + b == b + a

By convention, (+) is regarded as commutative, but this is not universal, and the introduction of another symbol which means non-commutative addition seems a bit dogmatic.

>>> zero + 1
1

>>> 1 + 1
2

>>> 2 + zero == (2 :: Int)
True

>>> (1 + 2) + 3 == 1 + (2 + 3)
True

>>> 2 + 3 == 3 + 2
True

Compute the sum of a Foldable.

>>> sum [0..10]
55

Compute the accumulating sum of a Traversable.

>>> accsum [0..10]
[0,1,3,6,10,15,21,28,36,45,55]

or Subtraction

a - a == zero
negate a == zero - a
negate a + a == zero
a + negate a == zero

>>> negate 1
-1

>>> 1 - 2
-1

>>> 2 - 2 == (zero :: Int)
True

>>> negate 2 == zero - (2 :: Int)
True

>>> negate 2 + 2 == (zero :: Int)
True

>>> 2 + negate 2 == (zero :: Int)
True

or Multiplication

For practical reasons, we begin the class tree with Additive and Multiplicative. Starting with Associative and Unital, or using Semigroup and Monoid from base tends to confuse the interface once you start having to disinguish between (say) monoidal addition and monoidal multiplication.

one * a == a
a * one == a
(a * b) * c == a * (b * c)

By convention, (*) is regarded as not necessarily commutative, but this is not universal, and the introduction of another symbol which means commutative multiplication seems a bit dogmatic.

>>> one * 2
2

>>> 2 * 3
6

>>> 2 * one == (2 :: Int)
True

>>> (2 * 3) * 4 == 2 * (3 * 4)
True

Compute the product of a Foldable.

>>> product [1..5]
120

Compute the accumulating product of a Traversable.

>>> accproduct [1..5]
[1,2,6,24,120]

or Division

Though unusual, the term Divisive usefully fits in with the grammer of other classes and avoids name clashes that occur with some popular libraries.

a / a ~= one || a == zero
recip a ~= one / a || a == zero
recip a * a ~= one || a == zero
a * recip a ~= one || a == zero

>>> recip 2.0
0.5

>>> 1 / 2
0.5

>>> let a = 4.0 in a / a ~= one
True

>>> let a = 4.0 in recip a ~= one / a
True

>>> let a = 4.0 in recip a * a ~= one
True

>>> let a = 4.0 in a * recip a ~= one
True

Distributive

a * (b + c) == a * b + a * c
(a + b) * c == a * c + b * c
zero * a == zero
a * zero == zero

>>> 2 * (3 + 4) == 2 * 3 + 2 * 4
True

>>> (2 + 3) * 4 == 2 * 4 + 3 * 4
True

>>> zero * 2 == (zero :: Int)
True

>>> 2 * zero == (zero :: Int)
True

The sneaking in of the Absorption laws here glosses over the possibility that the multiplicative zero element does not have to correspond with the additive unital zero.

A Ring is an abelian group under addition (Unital, Associative, Commutative, Invertible) and monoidal under multiplication (Unital, Associative), and where multiplication distributes over addition.

\a -> zero + a == a
\a -> a + zero == a
\a b c -> (a + b) + c == a + (b + c)
\a b -> a + b == b + a
\a -> a - a == zero
\a -> negate a == zero - a
\a -> negate a + a == zero
\a -> a + negate a == zero
\a -> one * a == a
\a -> a * one == a
\a b c -> (a * b) * c == a * (b * c)
\a b c -> a * (b + c) == a * b + a * c
\a b c -> (a + b) * c == a * c + b * c
\a -> zero * a == zero
\a -> a * zero == zero

A StarSemiring is a semiring with a unary star operator satisfying the Conway equations:

\a -> star a == one + a * star a                                  -- fixpoint
\a b -> star (a * b) == one + a * star (b * a) * b                -- product-star (sliding)
\a b -> star (a + b) == star (star a * b) * star a                -- sum-star (vanishing)

These three equations are the doctestable core; they are exactly the sliding and vanishing axioms of a traced category in semiring clothing.

A Kleene Algebra is a Star Semiring with idempotent addition.

Idempotent addition gives a natural order a <= b ⟺ a + b == b. In that order, Kozen's induction laws hold as derived facts:

a * x + x <= x  ==>  star a * x + x <= x
x * a + x <= x  ==>  x * star a + x <= x

They are stated here as prose rather than class laws because they involve a partial order and Horn clauses, which do not fit the equational/doctest style of the Conway core.

Conway equations for Bool.

>>> let a = False; b = True in star (a * b) == one + a * star (b * a) * b
True

>>> let a = False; b = True in star (a + b) == star (star a * b) * star a
True

Involutive Ring

adj (a + b) ==> adj a + adj b
adj (a * b) ==> adj a * adj b
adj one ==> one
adj (adj a) ==> a

Note: elements for which adj a == a are called "self-adjoint".

Defining two requires adding the multiplicative unital to itself. In other words, the concept of two is a Ring one.

>>> two
2

Tropical (min-plus) semiring for Floyd–Warshall shortest paths.

Addition is min, multiplication is ordinary addition, the additive unit is positive infinity, and the multiplicative unit is zero.

>>> MinPlus 3 + MinPlus 2 :: MinPlus Double
MinPlus {getMinPlus = 2.0}

>>> MinPlus 3 * MinPlus 2 :: MinPlus Double
MinPlus {getMinPlus = 5.0}

Boolean semiring for Warshall's transitive closure.

plus is ||, times is &&, star is constantly True.

>>> Warshall True + Warshall False
Warshall True

A Field is a set on which addition, subtraction, multiplication, and division are defined. It is also assumed that multiplication is distributive over addition.

A summary of the rules inherited from super-classes of Field:

zero + a == a
a + zero == a
((a + b) + c) (a + (b + c))
a + b == b + a
a - a == zero
negate a == zero - a
negate a + a == zero
a + negate a == zero
one * a == a
a * one == a
((a * b) * c) == (a * (b * c))
(a * (b + c)) == (a * b + a * c)
((a + b) * c) == (a * c + b * c)
a * zero == zero
zero * a == zero
a / a == one || a == zero
recip a == one / a || a == zero
recip a * a == one || a == zero
a * recip a == one || a == zero

A hyperbolic field class

a < zero || (sqrt . (**2)) a == a
a < zero || (log . exp) a ~= a
b < zero || a <= zero || a == 1 || abs (a ** logBase a b - b) < 10 * epsilon

>>> (sqrt . (**2)) (4.0 :: Double) == 4.0
True

>>> (log . exp) (1.0 :: Double) ~= 1.0
True

>>> 2 ** logBase 2 8 ~= (8 :: Double)
True

Quotienting of a Field into a Ring

See Field of fractions

\a -> a - one < floor a <= a <= ceiling a < a + one

>>> properFraction (1.5 :: Double)
Quotient {whole = 1, fraction = 0.5}

>>> fromQuotient (properFraction (1.5 :: Double))
1.5

Whole-and-fraction pair. properFraction is the normalizer (Prelude toward-zero). The constructor is raw; the range is not enforced.

properFraction as the named normalizer into Quotient.

The canonical range is the Prelude toward-zero split: fraction ∈ (-1, 1) with the sign of the input, and fromQuotient (toQuotient a) == a.

Recombine a Quotient. Law: fromQuotient (toQuotient a) == a.

Bilinear multiplication of quotients: recombine, multiply, re-split.

(w1 + f1) * (w2 + f2) expands to the four terms w1*w2 + w1*f2 + f1*w2 + f1*f2, and toQuotient pushes any overflow back into whole. The same bilinear-then-normalize pattern as complex multiplication.

>>> mulQuotient (toQuotient (0.5 :: Double)) (toQuotient (3.0 :: Double))
Quotient {whole = 1, fraction = 0.5}

>>> mulQuotient (toQuotient (1.5 :: Double)) (toQuotient (2.0 :: Double)) == toQuotient (1.5 * 2.0 :: Double)
True

Trigonometric Field

The list of laws is quite long: trigonometric identities

infinity is defined for any Field.

>>> one / zero + infinity
Infinity

>>> infinity + 1
Infinity

negative infinity

>>> negInfinity + infinity
NaN

nan is defined as zero/zero

but note the (social) law:

>>> nan == zero / zero
False

A half of one

>>> half :: Double
0.5

Approximate modulo for fields

>>> modF 1.5 1.2
0.30000000000000004

Since: 0.13

Approximate diviso for fields.

Compared with div, divF returns the original type rather than the Whole type.

>>> divF 1.5 1.2
1.0

Since: 0.13

Approximate divMod for fields.

>>> divModF 1.5 1.2
DivMod {div_ = 1.0, mod_ = 0.30000000000000004}

Since: 0.13

A algebraic structure with element joins: See Semilattice

Associativity: x \/ (y \/ z) == (x \/ y) \/ z
Commutativity: x \/ y == y \/ x
Idempotency:   x \/ x == x