Groupoid.purs

-- | Binary operation
class Magma a where
  op ∷ a → a → a

-- | Associativity: `∀ a b. (a • b) • c = a • (b • c)`
class Magma a ⇐ Associative a

-- | Identity: `∀ a. a • identity = a && identity • a = a`
class Magma a ⇐ Identity a where
  identity ∷ a

-- | Inverse element: `∃ e. a • b = b • a = e`
class Magma a ⇐ Inverse a where
  inverse ∷ a → a

-- | Commutativity: `∀ a b. a • b = b • a`
class Magma a ⇐ Commutative a

-- | Idempotent: `∀ a. a • a = a`
class Magma a ⇐ Idempotent a

type Semigroup a = Associative a ⇒ Magma a ⇒ a
type Monoid a = Identity a ⇒ Semigroup a

type Band a = Idempotent a ⇒ Semigroup a
type Semilattice a = Commutative a ⇒ Band a

type Group a = Inverse a ⇒ Monoid a

type AbelianGroup a = Commutative a ⇒ Group a

@garyb Is there an issue/PR on a github project where I can watch discussion of this idea?