Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

A magma heirarchy for addition. The basic magma structure is repeated and prefixed with 'Additive-'.

- class AdditiveMagma a where
- class AdditiveMagma a => AdditiveUnital a where
- class AdditiveMagma a => AdditiveAssociative a
- class AdditiveMagma a => AdditiveCommutative a
- class AdditiveMagma a => AdditiveInvertible a where
- class AdditiveMagma a => AdditiveIdempotent a
- sum :: (Additive a, Foldable f) => f a -> a
- class (AdditiveCommutative a, AdditiveUnital a, AdditiveAssociative a) => Additive a where
- class (AdditiveUnital a, AdditiveAssociative a, AdditiveInvertible a) => AdditiveRightCancellative a where
- class (AdditiveUnital a, AdditiveAssociative a, AdditiveInvertible a) => AdditiveLeftCancellative a where
- class (Additive a, AdditiveInvertible a) => AdditiveGroup a where

# Documentation

class AdditiveMagma a where Source #

class AdditiveMagma a => AdditiveUnital a where Source #

Unital magma for addition.

zero `plus` a == a a `plus` zero == a

class AdditiveMagma a => AdditiveAssociative a Source #

Associative magma for addition.

(a `plus` b) `plus` c == a `plus` (b `plus` c)

class AdditiveMagma a => AdditiveCommutative a Source #

Commutative magma for addition.

a `plus` b == b `plus` a

class AdditiveMagma a => AdditiveInvertible a where Source #

Invertible magma for addition.

∀ a ∈ A: negate a ∈ A

law is true by construction in Haskell

class AdditiveMagma a => AdditiveIdempotent a Source #

Idempotent magma for addition.

a `plus` a == a

sum :: (Additive a, Foldable f) => f a -> a Source #

sum definition avoiding a clash with the Sum monoid in base

class (AdditiveCommutative a, AdditiveUnital a, AdditiveAssociative a) => Additive a where Source #

Additive is commutative, unital and associative under addition

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

class (AdditiveUnital a, AdditiveAssociative a, AdditiveInvertible a) => AdditiveRightCancellative a where Source #

Non-commutative right minus

a `plus` negate a = zero

class (AdditiveUnital a, AdditiveAssociative a, AdditiveInvertible a) => AdditiveLeftCancellative a where Source #

Non-commutative left minus

negate a `plus` a = zero

class (Additive a, AdditiveInvertible a) => AdditiveGroup a where Source #

Minus (`-`

) is reserved for where both the left and right cancellative laws hold. This then implies that the AdditiveGroup is also Abelian.

Syntactic unary negation - substituting "negate a" for "-a" in code - is hard-coded in the language to assume a Num instance. So, for example, using ''-a = zero - a' for the second rule below doesn't work.

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