commit 4442fcad3fba0446222e91d9d2052531f48d5f51
parent 166e07f464488e79fc091bd642aed744e39fe8b6
Author: Robert Russell <robert@rr3.xyz>
Date: Wed, 14 Oct 2026 21:27:16 -0700
Algebra.Magma: init (WIP)
Diffstat:
2 files changed, 756 insertions(+), 0 deletions(-)
diff --git a/src/Lude/Algebra.hs b/src/Lude/Algebra.hs
@@ -3,3 +3,4 @@ module Lude.Algebra (
) where
import Lude.Algebra.Category as X
+import Lude.Algebra.Magma as X
diff --git a/src/Lude/Algebra/Magma.hs b/src/Lude/Algebra/Magma.hs
@@ -0,0 +1,755 @@
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module Lude.Algebra.Magma (
+ -- * Magma tags
+ MagmaK,
+ Combinative,
+ Additive,
+ Multiplicative,
+
+ -- * Semigroups
+ IsSemigroup_ (..),
+ IsSemigroup,
+ combine,
+ (<>),
+ (⋄),
+ IsAddSemigroup,
+ add,
+ (+),
+ IsMulSemigroup,
+ mul,
+ (*),
+
+ -- * Partial cancellation
+ PartiallyLeftCancellable_ (..),
+ PartiallyRightCancellable_ (..),
+ PartiallyCancellable_,
+ PartiallyLeftCancellable,
+ cancelL',
+ (\\!),
+ PartiallyRightCancellable,
+ cancelR',
+ (//!),
+ PartiallyCancellable,
+ cancel',
+ PartiallyLeftSubtractable,
+ subtractL',
+ PartiallyRightSubtractable,
+ subtractR',
+ PartiallySubtractable,
+ subtract',
+ sub',
+ (-!),
+ PartiallyLeftDividable,
+ divideByL',
+ (\!),
+ PartiallyRightDividable,
+ divideByR',
+ (/!),
+ PartiallyDividable,
+ divideBy',
+
+ -- * Decidable cancellation
+ DecidablyLeftCancellable_ (..),
+ DecidablyRightCancellable_ (..),
+ DecidablyCancellable_,
+ DecidablyLeftCancellable,
+ tryCancelL#,
+ (\\?#),
+ tryCancelL,
+ (\\?),
+ DecidablyRightCancellable,
+ tryCancelR#,
+ (//?#),
+ tryCancelR,
+ (//?),
+ DecidablyCancellable,
+ tryCancel#,
+ tryCancel,
+ DecidablyLeftSubtractable,
+ trySubtractL#,
+ trySubtractL,
+ DecidablyRightSubtractable,
+ trySubtractR#,
+ trySubtractR,
+ DecidablySubtractable,
+ trySubtract#,
+ trySubtract,
+ DecidablyLeftDividable,
+ tryDivideByL#,
+ (\?#),
+ tryDivideByL,
+ (\?),
+ DecidablyRightDividable,
+ tryDivideByR#,
+ (/?#),
+ tryDivideByR,
+ (/?),
+ DecidablyDividable,
+ tryDivideBy#,
+ tryDivideBy,
+
+ -- * Monoids
+ IsMonoid_ (..),
+ IsMonoid,
+ neutral,
+ IsAddMonoid,
+ zero,
+ IsMulMonoid,
+ one,
+
+ -- * Partial inverses
+ PartiallyHasInverses_ (..),
+ PartiallyHasInverses,
+ invert',
+ PartiallyHasNegations,
+ negate',
+ PartiallyHasReciprocals,
+ recip',
+
+ -- * Decidable inverses
+ DecidablyHasInverses_ (..),
+ DecidablyHasInverses,
+ tryInvert#,
+ tryInvert,
+ DecidablyHasNegations,
+ tryNegate#,
+ tryNegate,
+ DecidablyHasReciprocals,
+ tryRecip#,
+ tryRecip,
+
+ -- * Groups
+ IsGroup_,
+ IsGroup,
+ cancelL,
+ -- TODO: Rename the conflicting (\\)
+ -- (\\),
+ cancelR,
+ (//),
+ invert,
+ IsAddGroup,
+ subtractL,
+ subtractR,
+ subtract,
+ sub,
+ (-),
+ negate,
+ IsMulGroup,
+ divideByL,
+ divideByR,
+ (/),
+ divideBy,
+ recip,
+
+ -- * Commutativity
+ Commutative_,
+ Commutative,
+ AddCommutative,
+ MulCommutative,
+ IsCommSemigroup,
+ IsCommAddSemigroup,
+ IsCommMulSemigroup,
+ IsCommMonoid,
+ IsCommAddMonoid,
+ IsCommMulMonoid,
+ IsCommGroup,
+ IsCommAddGroup,
+ IsCommMulGroup,
+
+ -- * Rings
+ IsSemiring,
+ IsCommSemiring,
+ IsRing,
+ IsCommRing,
+ IsDivisionRing,
+ IsField,
+) where
+
+import Data.Coerce
+import Numeric.Natural (Natural)
+import Numeric.Natural qualified as Base
+import Prelude (Integer, Rational)
+import Prelude qualified as Base
+
+import Lude.Algebra.Category.Core
+import Lude.Function
+import Lude.Haskell
+import Lude.Maybe
+
+-- TODO: The "magma" terminology is a bit wrong/misleading for the ring-like
+-- structures.
+
+-- TODO: Break this up.
+
+-- TODO: We should somehow connect these to the categorical abstractions, so
+-- that we don't have two abstraction islands. E.g., maybe all these should be
+-- required to form an Eilenberg-Moore algebra (except the truely
+-- "non-algebraic" ones, like fields).
+
+-- TODO: Should the initial rig/ring maps (out of Natural/Integer) use
+-- the categorical machinery for initial objects?
+
+-- TODO: newtype to view X as X-oid with one object, and vice versa.
+
+-- TODO: Should addition be commutative always? It conventionally is.
+
+-- TODO: Torsors
+
+-- TODO: Modular integers with arbitrary modulus (requires passing around
+-- modulus; see Oleg paper)
+
+-- TODO: Invertible/Unit type (newtype wrapper or pair) for the group of units,
+-- the non-oidified version of Iso
+
+-- TODO: Decidable sign for ordered ring-like things
+
+-- TODO: Left- and right- actions
+
+-- TODO: Localization / field of fractions / Ratio
+
+-- TODO: Euclidean div/mod
+
+-- TODO:
+-- type Exp :: forall {r :: Repr}. Type# r -> Type# r
+-- newtype Exp a = MkExp a
+-- type Log :: forall {r :: Repr}. Type# r -> Type# r
+-- newtype Log a = MkLog a
+
+--------------------------------------------------------------------------------
+
+data MagmaB :: Brand
+type MagmaK = OpenKind MagmaB
+
+-- The three standard magma tags.
+data Combinative :: MagmaK
+data Additive :: MagmaK
+data Multiplicative :: MagmaK
+
+--------------------------------------------------------------------------------
+-- Private Util
+
+type MagmaClass_ :: Kind
+type MagmaClass_ = MagmaK -> MagmaClass
+
+type MagmaClass :: Kind
+type MagmaClass = forall {r :: Repr}. Type# r -> Constraint
+
+type UnaryOp :: MagmaClass -> Type
+type UnaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => Endo a
+
+type UnaryOpMaybe# :: MagmaClass -> Type
+type UnaryOpMaybe# c = forall {r :: Repr} (a :: Type# r). (c a) => a -> Maybe# a
+
+type UnaryOpMaybe :: MagmaClass -> Type
+type UnaryOpMaybe c = forall (a :: Type). (c a) => a -> Maybe a
+
+type BinaryOp :: MagmaClass -> Type
+type BinaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => Biendo a
+
+type BinaryOpMaybe# :: MagmaClass -> Type
+type BinaryOpMaybe# c = forall {r :: Repr} (a :: Type# r). (c a) => a -> a -> Maybe# a
+
+type BinaryOpMaybe :: MagmaClass -> Type
+type BinaryOpMaybe c = forall (a :: Type). (c a) => a -> a -> Maybe a
+
+type Comm :: Endo MagmaClass_
+class (c this a, Commutative_ this a) => Comm c this (a :: Type# r)
+instance forall (c :: MagmaClass_) (this :: MagmaK) (r :: Repr) (a :: Type# r). (c this a, Commutative_ this a) => Comm c this a
+
+--------------------------------------------------------------------------------
+
+-- TODO: Remove Functional# superclass? We currently require it for some
+-- generic definitions, but we should probably allow any representation.
+
+-- | Semigroup
+--
+-- __Laws:__
+-- - /@combine@ is associative:/ @(x ⋄ y) ⋄ z = x ⋄ (y ⋄ z)@
+type IsSemigroup_ :: MagmaClass_
+class (Functional# r) => IsSemigroup_ this (a :: Type# r) where
+ combine_ :: For this (Biendo a)
+
+type IsSemigroup = IsSemigroup_ Combinative :: MagmaClass
+combine, (<>), (⋄) :: forall {r :: Repr} (a :: Type# r). (IsSemigroup a) => Biendo a
+combine = combine_ Combinative
+(<>) = combine
+(⋄) = combine
+infixl 5 <>, ⋄
+
+type IsAddSemigroup = IsSemigroup_ Additive :: MagmaClass
+add, (+) :: forall {r :: Repr} (a :: Type# r). (IsAddSemigroup a) => Biendo a
+add = combine_ Additive
+(+) = add
+infixl 6 +
+
+type IsMulSemigroup = IsSemigroup_ Multiplicative :: MagmaClass
+mul, (*) :: forall {r :: Repr} (a :: Type# r). (IsMulSemigroup a) => Biendo a
+mul = combine_ Multiplicative
+(*) = mul
+infixl 7 *
+
+--------------------------------------------------------------------------------
+
+-- TODO: Names suck here
+
+-- | Semigroup with computable left cancellation for left-cancellable elements
+--
+-- __Laws:__
+-- - /Partial left cancellation:/ if @x@ is left-cancellative, then @(x \\!) ∘ (x ⋄)@ = @identity@
+--
+-- We don't specify @(x \\!)@ on elements outside the image of @(x ⋄)@.
+--
+-- Typically, monoids should also implement `PartiallyHasInverses_`
+type PartiallyLeftCancellable_ :: MagmaClass_
+class (IsSemigroup_ this a) => PartiallyLeftCancellable_ this (a :: Type# r) where
+ cancelL'_ :: For this (Biendo a)
+
+-- | Semigroup with computable right cancellation for right-cancellable elements
+--
+-- __Laws:__
+-- - /Partial right cancellation:/ if @x@ is right-cancellative, then @(//! x) ∘ (⋄ x)@ = @identity@
+--
+-- We don't specify @(//! x)@ on elements outside the image of @(⋄ x)@.
+--
+-- Typically, monoids should also implement `PartiallyHasInverses_`
+type PartiallyRightCancellable_ :: MagmaClass_
+class (IsSemigroup_ this a) => PartiallyRightCancellable_ this (a :: Type# r) where
+ cancelR'_ :: For this (Biendo a)
+
+-- | Commutative semigroup with computable cancellation for cancellable elements
+type PartiallyCancellable_ :: MagmaClass_
+class (Commutative_ this a, PartiallyLeftCancellable_ this a, PartiallyRightCancellable_ this a) => PartiallyCancellable_ this (a :: Type# r)
+
+instance (Commutative_ this a, PartiallyLeftCancellable_ this a, PartiallyRightCancellable_ this a) => PartiallyCancellable_ this (a :: Type# r)
+
+type PartiallyLeftCancellable = PartiallyLeftCancellable_ Combinative :: MagmaClass
+cancelL', (\\!) :: BinaryOp PartiallyLeftCancellable
+cancelL' = cancelL'_ Combinative
+(\\!) = cancelL'
+infixr 5 \\!
+
+type PartiallyRightCancellable = PartiallyRightCancellable_ Combinative :: MagmaClass
+cancelR', (//!) :: BinaryOp PartiallyRightCancellable
+cancelR' = cancelR'_ Combinative
+(//!) = flip cancelR'
+infixl 5 //!
+
+type PartiallyCancellable = PartiallyCancellable_ Combinative :: MagmaClass
+cancel' :: BinaryOp PartiallyCancellable
+cancel' = cancelR'
+
+type PartiallyLeftSubtractable = PartiallyLeftCancellable_ Additive :: MagmaClass
+subtractL' :: BinaryOp PartiallyLeftSubtractable
+subtractL' = cancelL'_ Additive
+
+type PartiallyRightSubtractable = PartiallyRightCancellable_ Additive :: MagmaClass
+subtractR' :: BinaryOp PartiallyRightSubtractable
+subtractR' = cancelR'_ Additive
+
+-- NOTE: There're no standard symbols for left/right-subtraction, because
+-- usually one assumes additive operations are commutative. So we just
+-- require commutativity for the subtraction symbols.
+
+type PartiallySubtractable = PartiallyCancellable_ Additive :: MagmaClass
+subtract', sub', (-!) :: BinaryOp PartiallySubtractable
+subtract' = subtractR'
+sub' = flip subtract'
+(-!) = sub'
+infixl 6 -!
+
+type PartiallyLeftDividable = PartiallyLeftCancellable_ Multiplicative :: MagmaClass
+divideByL', (\!) :: BinaryOp PartiallyLeftDividable
+divideByL' = cancelL'_ Multiplicative
+(\!) = divideByL'
+infixr 7 \!
+
+type PartiallyRightDividable = PartiallyRightCancellable_ Multiplicative :: MagmaClass
+divideByR', (/!) :: BinaryOp PartiallyRightDividable
+divideByR' = cancelR'_ Multiplicative
+(/!) = flip divideByR'
+infixl 7 /!
+
+type PartiallyDividable = PartiallyCancellable_ Multiplicative :: MagmaClass
+divideBy' :: BinaryOp PartiallyDividable
+divideBy' = divideByR'
+
+--------------------------------------------------------------------------------
+
+-- | Semigroup with "decidable left cancellation" (i.e., decidable
+-- left-cancellability and decidable images of left-combination with
+-- left-cancellable elements)
+--
+-- __Laws:__
+-- - /Decidable left cancellation:/ if @x@ is left-cancellative and @y@
+-- factors (necessarily uniquely) as @y = x ⋄ z@, then @x \\? y@ =
+-- @Just z@; otherwise, @x \\? y@ = @Nothing@
+--
+-- Typically, monoids should also implement `DecidablyHasInverses_`
+type DecidablyLeftCancellable_ :: MagmaClass_
+class (PartiallyLeftCancellable_ this a) => DecidablyLeftCancellable_ this (a :: Type# r) where
+ tryCancelL_# :: For this (a -> a -> Maybe# a)
+
+-- | Semigroup with "decidable right cancellation" (i.e., decidable
+-- right-cancellability and decidable images of right-combination with
+-- right-cancellable elements)
+--
+-- __Laws:__
+-- - /Decidable right cancellation:/ if @x@ is right-cancellative and @y@
+-- factors (necessarily uniquely) as @y = z ⋄ x@, then @y //? x@ =
+-- @Just z@; otherwise, @y //? x@ = @Nothing@
+--
+-- Typically, monoids should also implement `DecidablyHasInverses_`
+type DecidablyRightCancellable_ :: MagmaClass_
+class (PartiallyRightCancellable_ this a) => DecidablyRightCancellable_ this (a :: Type# r) where
+ tryCancelR_# :: For this (a -> a -> Maybe# a)
+
+-- | Commutative semigroup with "decidable cancellation" (i.e., decidable
+-- cancellability and decidable images of combination with cancellable elements)
+type DecidablyCancellable_ :: MagmaClass_
+class (Commutative_ this a, DecidablyLeftCancellable_ this a, DecidablyRightCancellable_ this a) => DecidablyCancellable_ this (a :: Type# r)
+
+instance (Commutative_ this a, DecidablyLeftCancellable_ this a, DecidablyRightCancellable_ this a) => DecidablyCancellable_ this (a :: Type# r)
+
+type DecidablyLeftCancellable = DecidablyLeftCancellable_ Combinative :: MagmaClass
+tryCancelL#, (\\?#) :: BinaryOpMaybe# DecidablyLeftCancellable
+tryCancelL, (\\?) :: BinaryOpMaybe DecidablyLeftCancellable
+tryCancelL# = tryCancelL_# Combinative
+(\\?#) = tryCancelL#
+tryCancelL = coerce tryCancelL#
+(\\?) = tryCancelL
+infix 5 \\?#, \\?
+
+type DecidablyRightCancellable = DecidablyRightCancellable_ Combinative :: MagmaClass
+tryCancelR#, (//?#) :: BinaryOpMaybe# DecidablyRightCancellable
+tryCancelR, (//?) :: BinaryOpMaybe DecidablyRightCancellable
+tryCancelR# = tryCancelR_# Combinative
+(//?#) = flip tryCancelR#
+tryCancelR = coerce tryCancelR#
+(//?) = flip tryCancelR
+infix 5 //?#, //?
+
+type DecidablyCancellable = DecidablyCancellable_ Combinative :: MagmaClass
+tryCancel# :: BinaryOpMaybe# DecidablyCancellable
+tryCancel :: BinaryOpMaybe DecidablyCancellable
+tryCancel# = tryCancelR#
+tryCancel = tryCancelR
+
+type DecidablyLeftSubtractable = DecidablyLeftCancellable_ Additive :: MagmaClass
+trySubtractL# :: BinaryOpMaybe# DecidablyLeftSubtractable
+trySubtractL :: BinaryOpMaybe DecidablyLeftSubtractable
+trySubtractL# = tryCancelL_# Additive
+trySubtractL = coerce trySubtractL#
+
+type DecidablyRightSubtractable = DecidablyRightCancellable_ Additive :: MagmaClass
+trySubtractR# :: BinaryOpMaybe# DecidablyRightSubtractable
+trySubtractR :: BinaryOpMaybe DecidablyRightSubtractable
+trySubtractR# = tryCancelR_# Additive
+trySubtractR = coerce trySubtractR#
+
+type DecidablySubtractable = DecidablyCancellable_ Additive :: MagmaClass
+trySubtract# :: BinaryOpMaybe# DecidablySubtractable
+trySubtract :: BinaryOpMaybe DecidablySubtractable
+trySubtract# = trySubtractR#
+trySubtract = trySubtractR
+
+type DecidablyLeftDividable = DecidablyLeftCancellable_ Multiplicative :: MagmaClass
+tryDivideByL#, (\?#) :: BinaryOpMaybe# DecidablyLeftDividable
+tryDivideByL, (\?) :: BinaryOpMaybe DecidablyLeftDividable
+tryDivideByL# = tryCancelL_# Multiplicative
+(\?#) = tryDivideByL#
+tryDivideByL = coerce tryDivideByL#
+(\?) = tryDivideByL
+infix 7 \?#, \?
+
+type DecidablyRightDividable = DecidablyRightCancellable_ Multiplicative :: MagmaClass
+tryDivideByR#, (/?#) :: BinaryOpMaybe# DecidablyRightDividable
+tryDivideByR, (/?) :: BinaryOpMaybe DecidablyRightDividable
+tryDivideByR# = tryCancelR_# Multiplicative
+(/?#) = flip tryDivideByR#
+tryDivideByR = coerce tryDivideByR#
+(/?) = flip tryDivideByR
+infix 7 /?#, /?
+
+type DecidablyDividable = DecidablyCancellable_ Multiplicative :: MagmaClass
+tryDivideBy# :: BinaryOpMaybe# DecidablyDividable
+tryDivideBy :: BinaryOpMaybe DecidablyDividable
+tryDivideBy# = tryDivideByR#
+tryDivideBy = tryDivideByR
+
+--------------------------------------------------------------------------------
+
+-- | Monoid
+--
+-- __Laws:__
+-- - /@neutral@ is a (left and right) identity element:/ @neutral ⋄ x = x = x ⋄ neutral@
+type IsMonoid_ :: MagmaClass_
+class (IsSemigroup_ this a) => IsMonoid_ this (a :: Type# r) where
+ neutral_ :: For this a
+
+type IsMonoid = IsMonoid_ Combinative :: MagmaClass
+neutral :: forall {r :: Repr} (a :: Type# r). (IsMonoid a) => a
+neutral = neutral_ Combinative
+
+type IsAddMonoid = IsMonoid_ Additive :: MagmaClass
+zero :: forall {r :: Repr} (a :: Type# r). (IsAddMonoid a) => a
+zero = neutral_ Additive
+
+type IsMulMonoid = IsMonoid_ Multiplicative :: MagmaClass
+one :: forall {r :: Repr} (a :: Type# r). (IsMulMonoid a) => a
+one = neutral_ Multiplicative
+
+--------------------------------------------------------------------------------
+
+-- NOTE: One-sided (left/right) inverses are noncanonical (and apparently not
+-- very useful, anyway), so we only model two-sided inverses.
+
+-- | Monoid with computable inverses for invertible elements
+--
+-- __Laws:__
+-- - /Partial inversion:/ if @x@ has inverse @y@, then @invert' x = y@
+--
+-- We don't specify @invert'@ on non-invertible elements.
+type PartiallyHasInverses_ :: MagmaClass_
+class (IsMonoid_ this a) => PartiallyHasInverses_ this (a :: Type# r) where
+ invert'_ :: For this (Endo a)
+
+type PartiallyHasInverses = PartiallyHasInverses_ Combinative :: MagmaClass
+invert' :: UnaryOp PartiallyHasInverses
+invert' = invert'_ Combinative
+
+type PartiallyHasNegations = PartiallyHasInverses_ Additive :: MagmaClass
+negate' :: UnaryOp PartiallyHasNegations
+negate' = invert'_ Additive
+
+type PartiallyHasReciprocals = PartiallyHasInverses_ Multiplicative :: MagmaClass
+recip' :: UnaryOp PartiallyHasReciprocals
+recip' = invert'_ Multiplicative
+
+--------------------------------------------------------------------------------
+
+-- | Monoid with decidable invertibility and computable inverses for invertible
+-- elements
+--
+-- __Laws:__
+-- - /Decidable inversion:/ if @x@ has inverse @y@, then @tryInvert x@ =
+-- @Just y@; otherwise, @tryInvert x = Nothing@
+type DecidablyHasInverses_ :: MagmaClass_
+class (PartiallyHasInverses_ this a) => DecidablyHasInverses_ this (a :: Type# r) where
+ tryInvert_# :: For this (a -> Maybe# a)
+
+type DecidablyHasInverses = DecidablyHasInverses_ Combinative :: MagmaClass
+tryInvert# :: UnaryOpMaybe# DecidablyHasInverses
+tryInvert :: UnaryOpMaybe DecidablyHasInverses
+tryInvert# = tryInvert_# Combinative
+tryInvert = coerce tryInvert#
+
+type DecidablyHasNegations = DecidablyHasInverses_ Additive :: MagmaClass
+tryNegate# :: UnaryOpMaybe# DecidablyHasNegations
+tryNegate :: UnaryOpMaybe DecidablyHasNegations
+tryNegate# = tryInvert_# Additive
+tryNegate = coerce tryNegate#
+
+type DecidablyHasReciprocals = DecidablyHasInverses_ Multiplicative :: MagmaClass
+tryRecip# :: UnaryOpMaybe# DecidablyHasReciprocals
+tryRecip :: UnaryOpMaybe DecidablyHasReciprocals
+tryRecip# = tryInvert_# Multiplicative
+tryRecip = coerce tryRecip#
+
+--------------------------------------------------------------------------------
+
+-- | Group
+--
+-- __Laws:__
+-- - /Every element is invertible:/ @isJust (tryInvert x)@ = @True@
+type IsGroup_ :: MagmaClass_
+class (DecidablyHasInverses_ this a, DecidablyLeftCancellable_ this a, DecidablyRightCancellable_ this a) => IsGroup_ this (a :: Type# r)
+
+type IsGroup = IsGroup_ Combinative :: MagmaClass
+cancelL, (\\), cancelR, (//) :: BinaryOp IsGroup
+invert :: UnaryOp IsGroup
+cancelL = cancelL'
+(\\) = (\\!)
+cancelR = cancelR'
+(//) = (//!)
+invert = invert'
+infixr 5 \\
+infixl 5 //
+
+type IsAddGroup = IsGroup_ Additive :: MagmaClass
+subtractL, subtractR :: BinaryOp IsAddGroup
+subtract, sub, (-) :: BinaryOp IsCommAddGroup
+negate :: UnaryOp IsAddGroup
+subtractL = subtractL'
+subtractR = subtractR'
+subtract = subtract'
+sub = sub'
+(-) = (-!)
+negate = negate'
+infixl 6 -
+
+type IsMulGroup = IsGroup_ Multiplicative :: MagmaClass
+divideByL, divideByR, (/) :: BinaryOp IsMulGroup -- NOTE: (\) is reserved in Haskell :(
+divideBy :: BinaryOp IsCommMulGroup
+recip :: UnaryOp IsMulGroup
+divideByL = divideByL'
+divideByR = divideByR'
+(/) = (/!)
+divideBy = divideBy'
+recip = recip'
+infixl 7 /
+
+--------------------------------------------------------------------------------
+
+-- | Commutative semigroup
+--
+-- __Laws:__
+-- - /@combine@ is commutative:/ @x ⋄ y = y ⋄ x@
+type Commutative_ :: MagmaClass_
+class (IsSemigroup_ this a) => Commutative_ this (a :: Type# r)
+
+type Commutative = Commutative_ Combinative :: MagmaClass
+type AddCommutative = Commutative_ Additive :: MagmaClass
+type MulCommutative = Commutative_ Multiplicative :: MagmaClass
+
+type IsCommSemigroup = Comm IsSemigroup_ Combinative :: MagmaClass
+type IsCommAddSemigroup = Comm IsSemigroup_ Additive :: MagmaClass
+type IsCommMulSemigroup = Comm IsSemigroup_ Multiplicative :: MagmaClass
+
+type IsCommMonoid = Comm IsMonoid_ Combinative :: MagmaClass
+type IsCommAddMonoid = Comm IsMonoid_ Additive :: MagmaClass
+type IsCommMulMonoid = Comm IsMonoid_ Multiplicative :: MagmaClass
+
+type IsCommGroup = Comm IsGroup_ Combinative :: MagmaClass
+type IsCommAddGroup = Comm IsGroup_ Additive :: MagmaClass
+type IsCommMulGroup = Comm IsGroup_ Multiplicative :: MagmaClass
+
+--------------------------------------------------------------------------------
+
+-- TODO: Generalize to take two MagmaK's
+
+-- TODO: Laws
+
+-- TODO: DecidableZero for decidable division rings (and fields)?
+
+type IsSemiring :: MagmaClass
+class (IsCommAddMonoid a, IsMulMonoid a) => IsSemiring (a :: Type# r)
+
+type IsCommSemiring :: MagmaClass
+class (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r)
+instance (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r)
+
+type IsRing :: MagmaClass
+class (IsSemiring a, IsAddGroup a) => IsRing (a :: Type# r)
+
+type IsCommRing :: MagmaClass
+class (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r)
+instance (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r)
+
+type IsDivisionRing :: MagmaClass
+class (IsRing a, PartiallyLeftDividable a, PartiallyRightDividable a, PartiallyHasReciprocals a) => IsDivisionRing a
+
+type IsField :: MagmaClass
+class (IsDivisionRing a, MulCommutative a) => IsField a
+instance (IsDivisionRing a, MulCommutative a) => IsField a
+
+--------------------------------------------------------------------------------
+
+baseZero :: (Base.Num a) => a
+baseZero = 0 where fromInteger = Base.fromInteger
+
+baseOne :: (Base.Num a) => a
+baseOne = 1 where fromInteger = Base.fromInteger
+
+instance (Base.Num a) => IsSemigroup_ Additive (BaseInterop a) where combine_ _ = coerce (Base.+)
+instance (Base.Num a) => PartiallyLeftCancellable_ Additive (BaseInterop a) where cancelL'_ _ = coerce Base.subtract
+instance (Base.Num a) => DecidablyLeftCancellable_ Additive (BaseInterop a) where tryCancelL_# _ = coerce $ Just .* Base.subtract
+instance (Base.Num a) => PartiallyRightCancellable_ Additive (BaseInterop a) where cancelR'_ _ = coerce Base.subtract
+instance (Base.Num a) => DecidablyRightCancellable_ Additive (BaseInterop a) where tryCancelR_# _ = coerce $ Just .* Base.subtract
+instance (Base.Num a) => PartiallyHasInverses_ Additive (BaseInterop a) where invert'_ _ = coerce Base.negate
+instance (Base.Num a) => DecidablyHasInverses_ Additive (BaseInterop a) where tryInvert_# _ = coerce $ Just . Base.negate
+instance (Base.Num a) => IsMonoid_ Additive (BaseInterop a) where neutral_ _ = coerce baseZero
+instance (Base.Num a) => IsGroup_ Additive (BaseInterop a)
+instance (Base.Num a) => Commutative_ Additive (BaseInterop a)
+instance (Base.Num a) => IsSemigroup_ Multiplicative (BaseInterop a) where combine_ _ = coerce (Base.*)
+instance (Base.Num a) => IsMonoid_ Multiplicative (BaseInterop a) where neutral_ _ = coerce baseOne
+instance (Base.Num a) => IsSemiring (BaseInterop a)
+instance (Base.Num a) => IsRing (BaseInterop a)
+instance (Base.Fractional a) => PartiallyLeftCancellable_ Multiplicative (BaseInterop a) where cancelL'_ _ = coerce \x y -> Base.recip x Base.* y
+instance (Base.Fractional a) => PartiallyRightCancellable_ Multiplicative (BaseInterop a) where cancelR'_ _ = coerce $ flip (Base./)
+instance (Base.Fractional a) => PartiallyHasInverses_ Multiplicative (BaseInterop a) where invert'_ _ = coerce Base.recip
+instance (Base.Fractional a) => IsDivisionRing (BaseInterop a)
+
+--------------------------------------------------------------------------------
+
+baseDivNonZero :: forall (a :: Type). (Base.Eq a, Base.Fractional a) => a -> a -> Maybe a
+baseDivNonZero x y = if y Base.== baseZero then Nothing else Just (x Base./ y)
+
+baseRecipNonZero :: forall (a :: Type). (Base.Eq a, Base.Fractional a) => a -> Maybe a
+baseRecipNonZero x = if x Base.== baseZero then Nothing else Just (Base.recip x)
+
+deriving via BaseInterop Natural instance IsSemigroup_ Additive Natural
+deriving via BaseInterop Natural instance PartiallyLeftCancellable_ Additive Natural
+instance DecidablyLeftCancellable_ Additive Natural where tryCancelL_# _ = coerce $ flip Base.minusNaturalMaybe
+deriving via BaseInterop Natural instance PartiallyRightCancellable_ Additive Natural
+instance DecidablyRightCancellable_ Additive Natural where tryCancelR_# _ = coerce $ flip Base.minusNaturalMaybe
+deriving via BaseInterop Natural instance IsMonoid_ Additive Natural
+deriving via BaseInterop Natural instance Commutative_ Additive Natural
+deriving via BaseInterop Natural instance IsSemigroup_ Multiplicative Natural
+deriving via BaseInterop Natural instance IsMonoid_ Multiplicative Natural
+instance Commutative_ Multiplicative Natural
+deriving via BaseInterop Natural instance IsSemiring Natural
+
+deriving via BaseInterop Integer instance IsSemigroup_ Additive Integer
+deriving via BaseInterop Integer instance PartiallyLeftCancellable_ Additive Integer
+deriving via BaseInterop Integer instance DecidablyLeftCancellable_ Additive Integer
+deriving via BaseInterop Integer instance PartiallyRightCancellable_ Additive Integer
+deriving via BaseInterop Integer instance DecidablyRightCancellable_ Additive Integer
+deriving via BaseInterop Integer instance IsMonoid_ Additive Integer
+deriving via BaseInterop Integer instance PartiallyHasInverses_ Additive Integer
+deriving via BaseInterop Integer instance DecidablyHasInverses_ Additive Integer
+deriving via BaseInterop Integer instance IsGroup_ Additive Integer
+deriving via BaseInterop Integer instance Commutative_ Additive Integer
+deriving via BaseInterop Integer instance IsSemigroup_ Multiplicative Integer
+deriving via BaseInterop Integer instance IsMonoid_ Multiplicative Integer
+instance Commutative_ Multiplicative Integer
+deriving via BaseInterop Integer instance IsSemiring Integer
+deriving via BaseInterop Integer instance IsRing Integer
+
+deriving via BaseInterop Rational instance IsSemigroup_ Additive Rational
+deriving via BaseInterop Rational instance PartiallyLeftCancellable_ Additive Rational
+deriving via BaseInterop Rational instance DecidablyLeftCancellable_ Additive Rational
+deriving via BaseInterop Rational instance PartiallyRightCancellable_ Additive Rational
+deriving via BaseInterop Rational instance DecidablyRightCancellable_ Additive Rational
+deriving via BaseInterop Rational instance IsMonoid_ Additive Rational
+deriving via BaseInterop Rational instance PartiallyHasInverses_ Additive Rational
+deriving via BaseInterop Rational instance DecidablyHasInverses_ Additive Rational
+deriving via BaseInterop Rational instance IsGroup_ Additive Rational
+deriving via BaseInterop Rational instance Commutative_ Additive Rational
+deriving via BaseInterop Rational instance IsSemigroup_ Multiplicative Rational
+deriving via BaseInterop Rational instance IsMonoid_ Multiplicative Rational
+instance Commutative_ Multiplicative Rational
+deriving via BaseInterop Rational instance IsSemiring Rational
+deriving via BaseInterop Rational instance IsRing Rational
+deriving via BaseInterop Rational instance PartiallyLeftCancellable_ Multiplicative Rational
+instance DecidablyLeftCancellable_ Multiplicative Rational where tryCancelL_# _ = coerce $ flip baseDivNonZero
+deriving via BaseInterop Rational instance PartiallyRightCancellable_ Multiplicative Rational
+instance DecidablyRightCancellable_ Multiplicative Rational where tryCancelR_# _ = coerce $ flip baseDivNonZero
+deriving via BaseInterop Rational instance PartiallyHasInverses_ Multiplicative Rational
+instance DecidablyHasInverses_ Multiplicative Rational where tryInvert_# _ = coerce baseRecipNonZero
+deriving via BaseInterop Rational instance IsDivisionRing Rational
+
+-- TODO: Switch-out base combinators for Lude's
+instance (IsSemigroup_ this a) => IsSemigroup_ this (r -> a) where combine_ _ = Base.liftA2 (combine_ this)
+instance (PartiallyLeftCancellable_ this a) => PartiallyLeftCancellable_ this (r -> a) where cancelL'_ _ = Base.liftA2 (cancelL'_ this)
+instance (PartiallyRightCancellable_ this a) => PartiallyRightCancellable_ this (r -> a) where cancelR'_ _ = Base.liftA2 (cancelR'_ this)
+instance (IsMonoid_ this a) => IsMonoid_ this (r -> a) where neutral_ _ = Base.const (neutral_ this)
+instance (PartiallyHasInverses_ this a) => PartiallyHasInverses_ this (r -> a) where invert'_ _ = Base.fmap (invert'_ this)
+instance (IsGroup_ this a) => DecidablyLeftCancellable_ this (r -> a) where tryCancelL_# _ = just# .* cancelL'_ this
+instance (IsGroup_ this a) => DecidablyRightCancellable_ this (r -> a) where tryCancelR_# _ = just# .* cancelR'_ this
+instance (IsGroup_ this a) => DecidablyHasInverses_ this (r -> a) where tryInvert_# _ = just# . invert'_ this
+instance (IsGroup_ this a) => IsGroup_ this (r -> a)
+instance (Commutative_ this a) => Commutative_ this (r -> a)
+instance (IsSemiring a) => IsSemiring (r -> a)
+instance (IsRing a) => IsRing (r -> a)
