Skip to content

Instantly share code, notes, and snippets.

@garyb
Created August 27, 2017 22:56
Show Gist options
  • Save garyb/cd979eef055121fc0b6a85a78d0ba3a0 to your computer and use it in GitHub Desktop.
Save garyb/cd979eef055121fc0b6a85a78d0ba3a0 to your computer and use it in GitHub Desktop.
-- | 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
@chexxor
Copy link

chexxor commented Aug 31, 2017

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment