| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
NumHask.Algebra.Additive
Description
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 #
plus is used as the operator for the additive magma to distinguish from + which, by convention, implies commutativity
∀ a,b ∈ A: a `plus` b ∈ A
law is true by construction in Haskell
Minimal complete definition
Instances
class AdditiveMagma a => AdditiveUnital a where Source #
Unital magma for addition.
zero `plus` a == a a `plus` zero == a
Minimal complete definition
Instances
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
Minimal complete definition
class AdditiveMagma a => AdditiveIdempotent a Source #
Idempotent magma for addition.
a `plus` a == a
Instances
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
Instances