|
15 | 15 | module Data.Group where |
16 | 16 |
|
17 | 17 | import Data.Monoid (class Monoid) |
| 18 | +import Data.Monoid.Dual (Dual(..)) |
18 | 19 | import Data.Ring (class Ring, negate) |
19 | 20 | import Data.Monoid.Additive (Additive(..)) |
| 21 | +import Data.Unit (Unit, unit) |
20 | 22 |
|
21 | 23 | -- | A `Group` is a `Monoid` with inverses. Instances |
22 | 24 | -- | must satisfy the following law in addition to the monoid laws: |
23 | 25 | -- | |
24 | | --- | ```text |
25 | | --- | forall x. ginverse x <> x = mempty = x <> ginverse x |
26 | | --- | ``` |
| 26 | +-- | - Inverse: `forall x. ginverse x <> x = mempty = x <> ginverse x` |
27 | 27 | class Monoid g <= Group g where |
28 | 28 | ginverse :: g -> g |
29 | 29 |
|
30 | | --- | A `CommutativeGroup` is a `Group` with a commutative monoid operation. |
31 | | --- | Instances must satisfy the following law in addition to the group laws: |
| 30 | +-- | A `CommutativeGroup` is a `Group` with a commutative semigroup operation. |
| 31 | +-- | Also known as an Abelian group. Instances must satisfy the following law |
| 32 | +-- | in addition to the group laws: |
32 | 33 | -- | |
33 | | --- | ```text |
34 | | --- | forall x, y. x <> y = y <> x |
35 | | --- | ``` |
| 34 | +-- | - Commutativity: `forall x, y. x <> y = y <> x` |
36 | 35 | class Group g <= CommutativeGroup g |
37 | 36 |
|
| 37 | +instance unitIsGroup :: Group Unit where |
| 38 | + ginverse _ = unit |
| 39 | + |
| 40 | +instance unitIsCommutativeGroup :: CommutativeGroup Unit |
| 41 | + |
| 42 | +instance dualGroupsAreGroups :: (Group g) => Group (Dual g) where |
| 43 | + ginverse (Dual x) = Dual (ginverse x) |
| 44 | + |
| 45 | +instance dualCommutativeGroupsAreCommutativeGroups :: (CommutativeGroup g) => CommutativeGroup (Dual g) |
| 46 | + |
38 | 47 | instance ringsAreAdditiveGroups :: (Ring r) => Group (Additive r) where |
39 | 48 | ginverse (Additive x) = Additive (negate x) |
40 | 49 |
|
|
0 commit comments