$\forall a \in R: (z + a) \sim a$

A (pre-)semiring with a right-neutral additive sunit must satisfy:

neutral_addition mempty ~~ const True

Or, equivalently:

mempty <> r ~~ r

This is a required property.

$\forall a \in R: (o * a) \sim a$

A (pre-)semiring with a right-neutral multiplicative sunit must satisfy:

neutral_multiplication sunit ~~ const True

Or, equivalently:

sunit >< r ~~ r

This is a required property.

$\forall a, b, c \in R: (a + b) + c \sim a + (b + c)$

R must right-associate addition.

This should be verified by the underlying Semigroup instance, but is included here for completeness.

This is a required property.

$\forall a, b, c \in R: (a * b) * c \sim a * (b * c)$

R must right-associate multiplication.

This is a required property.

$\forall a, b, c \in R: (a + b) * c \sim (a * c) + (b * c)$

R must right-distribute multiplication.

When R is a functor and the semiring structure is derived from Alternative, this translates to:

(a <|> b) *> c = (a *> c) <|> (b *> c)

See https://en.wikibooks.org/wiki/Haskell/Alternative_and_MonadPlus.

This is a required property.

$\forall a, b \in R: a * b \sim a * b + b$

If R is non-unital (i.e. sunit is not distinct from mempty) then it will instead satisfy a right-absorbtion property.

This follows from right-neutrality and right-distributivity.

Compare codistributive and closed_stable.

When R is also left-distributive we get: $\forall a, b \in R: a * b = a + a * b + b$

See also Warning and https://blogs.ncl.ac.uk/andreymokhov/united-monoids/#whatif.

$\forall a \in R: (z * a) \sim u$

A R is unital then its addititive sunit must be right-annihilative, i.e.:

mempty >< a ~~ mempty

For Alternative instances this property translates to:

empty *> a ~~ empty

All right semirings must have a right-absorbative addititive sunit, however note that depending on the Prd instance this does not preclude IEEE754-mandated behavior such as:

mempty >< NaN ~~ NaN

This is a required property.

fromBoolean must be a semiring homomorphism into R.

This is a required property.

$\forall a, b, c \in R: b + a \sim c + a \Rightarrow b = c$

If R is right-cancellative wrt addition then for all a the section (a <>) is injective.

$\forall a, b, c \in R: b * a \sim c * a \Rightarrow b = c$

If R is right-cancellative wrt multiplication then for all a the section (a ><) is injective.

$\forall a, b \in R: a + b \sim b + a$

$\forall a, b \in R: a * b \sim b * a$

$\forall M \geq 0; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b$

R must right-distribute multiplication between finite sums.

For types with exact arithmetic this follows from distributive & neutral_multiplication.

$\forall M \geq 1; a_1 \dots a_M, b \in R: (\sum_{i=1}^M a_i) * b \sim \sum_{i=1}^M a_i * b$

R must right-distribute multiplication over finite (non-empty) sums.

For types with exact arithmetic this follows from distributive and the universality of fold1.

$\forall M,N \geq 0; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) \sim \sum_{i=1 j=1}^{i=M j=N} a_i * b_j$

If R is also left-distributive then it supports cross-multiplication.

$\forall M,N \geq 1; a_1 \dots a_M, b_1 \dots b_N \in R: (\sum_{i=1}^M a_i) * (\sum_{j=1}^N b_j) = \sum_{i=1 j=1}^{i=M j=N} a_i * b_j$

If R is also left-distributive then it supports (non-empty) cross-multiplication.