commit c15bc6c5431ec7c8edf018c294551f08d943a536
parent 99272a8cfadf876e5a5630cb638b85c2ca6c1296
Author: Robert Russell <robert@rr3.xyz>
Date: Thu, 15 Oct 2026 21:10:22 -0700
Algebra.Magma: rename/refactor to make less clunky
Diffstat:
1 file changed, 450 insertions(+), 407 deletions(-)
diff --git a/src/Lude/Algebra/Magma.hs b/src/Lude/Algebra/Magma.hs
@@ -2,14 +2,14 @@
{-# LANGUAGE UndecidableSuperClasses #-}
module Lude.Algebra.Magma (
- -- * Magma tags
- MagmaK,
- Combinative,
- Additive,
- Multiplicative,
+ -- * Magma operations
+ MagmaOpK,
+ Combination,
+ Addition,
+ Multiplication,
-- * Semigroups
- IsSemigroup_ (..),
+ IsSemigroupWith (..),
IsSemigroup,
combine,
(<>),
@@ -22,97 +22,102 @@ module Lude.Algebra.Magma (
(*),
-- * Partial cancellation
- PartiallyCancellableL_ (..),
- PartiallyCancellableR_ (..),
- PartiallyCancellable_,
- PartiallyCancellableL,
- cancelL',
+ PartiallyCancellableL (..),
+ PartiallyCancellableR (..),
+ PartiallyCancellable,
+ PartiallyStrippableL,
+ pstripL,
(\\!),
- PartiallyCancellableR,
- cancelR',
+ PartiallyStrippableR,
+ pstripR,
(//!),
- PartiallyCancellable,
- cancel',
+ PartiallyStrippable,
+ pstrip,
PartiallySubtractableL,
- subtractL',
+ psubL,
PartiallySubtractableR,
- subtractR',
+ psubR,
PartiallySubtractable,
- subtract',
- sub',
+ psubtract,
+ psub,
(-!),
PartiallyDividableL,
- divideByL',
+ pdivL,
(\!),
PartiallyDividableR,
- divideByR',
+ pdivR,
(/!),
PartiallyDividable,
- divideBy',
+ pdiv,
-- * Decidable cancellation
- DecidablyCancellableL_ (..),
- DecidablyCancellableR_ (..),
- DecidablyCancellable_,
- DecidablyCancellableL,
- tryCancelL#,
- (\\?#),
+ DecidablyCancellableL (..),
tryCancelL,
+ DecidablyCancellableR (..),
+ tryCancelR,
+ DecidablyCancellable,
+ DecidablyStrippableL,
+ tryStripL#,
+ (\\?#),
+ tryStripL,
(\\?),
- DecidablyCancellableR,
- tryCancelR#,
+ DecidablyStrippableR,
+ tryStripR#,
(//?#),
- tryCancelR,
+ tryStripR,
(//?),
- DecidablyCancellable,
- tryCancel#,
- tryCancel,
+ DecidablyStrippable,
+ tryStrip#,
+ tryStrip,
DecidablySubtractableL,
- trySubtractL#,
- trySubtractL,
+ trySubL#,
+ trySubL,
DecidablySubtractableR,
- trySubtractR#,
- trySubtractR,
+ trySubR#,
+ trySubR,
DecidablySubtractable,
- trySubtract#,
- trySubtract,
+ trySub#,
+ (-?#),
+ trySub,
+ (-?),
DecidablyDividableL,
- tryDivideByL#,
+ tryDivL#,
(\?#),
- tryDivideByL,
+ tryDivL,
(\?),
DecidablyDividableR,
- tryDivideByR#,
+ tryDivR#,
(/?#),
- tryDivideByR,
+ tryDivR,
(/?),
DecidablyDividable,
- tryDivideBy#,
- tryDivideBy,
+ tryDiv#,
+ tryDiv,
-- * Monoids
- IsMonoid_ (..),
+ IsMonoidWith (..),
IsMonoid,
- neutral,
+ nil,
IsAddMonoid,
zero,
IsMulMonoid,
one,
-- * Partial inverses
- PartiallyHasInverses_ (..),
- PartiallyHasInverses,
- invert',
+ PartiallyHasInverses (..),
+ PartiallyHasUndos,
+ pundo,
PartiallyHasNegations,
- negate',
+ pnegate,
PartiallyHasReciprocals,
- recip',
+ precip,
-- * Decidable inverses
- DecidablyHasInverses_ (..),
- DecidablyHasInverses,
- tryInvert#,
+ DecidablyHasInverses (..),
tryInvert,
+ DecidablyHasUndos,
+ tryUndo#,
+ tryUndo,
DecidablyHasNegations,
tryNegate#,
tryNegate,
@@ -121,30 +126,33 @@ module Lude.Algebra.Magma (
tryRecip,
-- * Groups
- IsGroup_,
- IsGroup,
+ IsGroupWith,
cancelL,
+ cancelR,
+ invert,
+ IsGroup,
+ stripL,
-- TODO: Rename the conflicting (\\)
-- (\\),
- cancelR,
+ stripR,
(//),
- invert,
+ undo,
IsAddGroup,
- subtractL,
- subtractR,
+ subL,
+ subR,
subtract,
sub,
(-),
negate,
IsMulGroup,
- divideByL,
- divideByR,
+ divL,
+ divR,
(/),
- divideBy,
+ div,
recip,
-- * Commutativity
- Commutative_,
+ HasCommutative,
Commutative,
AddCommutative,
MulCommutative,
@@ -178,9 +186,6 @@ 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
@@ -219,411 +224,449 @@ import Lude.Maybe
--------------------------------------------------------------------------------
-data MagmaB :: Brand
-type MagmaK = OpenKind MagmaB
+data MagmaOpB :: Brand
--- The three standard magma tags.
-data Combinative :: MagmaK
-data Additive :: MagmaK
-data Multiplicative :: MagmaK
+-- | The `OpenKind` of magma operations
+--
+-- We index `MagmaClass`es by `MagmaOpK` to enable working generically over
+-- magmas that differ only in notation.
+--
+-- Lude has three standard magma operations:
+-- `Combination` (generic), `Addition`, and `Multiplication`.
+type MagmaOpK = OpenKind MagmaOpB
+
+data Combination :: MagmaOpK
+data Addition :: MagmaOpK
+data Multiplication :: MagmaOpK
--------------------------------------------------------------------------------
-- Private Util
-type MagmaClass_ :: Kind
-type MagmaClass_ = MagmaK -> MagmaClass
+type AlgebraClass :: Kind
+type AlgebraClass = forall {r :: Repr}. Type# r -> Constraint
type MagmaClass :: Kind
-type MagmaClass = forall {r :: Repr}. Type# r -> Constraint
+type MagmaClass = MagmaOpK -> AlgebraClass
+
+type NullaryOp :: AlgebraClass -> Type
+type NullaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => a
+
+type PartialUnaryOp :: AlgebraClass -> Type
+type PartialUnaryOp c = forall {r :: Repr} (a :: Type# r). (c a, Partial) => Endo a
-type UnaryOp :: MagmaClass -> Type
+type UnaryOp :: AlgebraClass -> Type
type UnaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => Endo a
-type UnaryOpMaybe# :: MagmaClass -> Type
+type UnaryOpMaybe# :: AlgebraClass -> Type
type UnaryOpMaybe# c = forall {r :: Repr} (a :: Type# r). (c a) => a -> Maybe# a
-type UnaryOpMaybe :: MagmaClass -> Type
+type UnaryOpMaybe :: AlgebraClass -> Type
type UnaryOpMaybe c = forall (a :: Type). (c a) => a -> Maybe a
-type BinaryOp :: MagmaClass -> Type
+type PartialBinaryOp :: AlgebraClass -> Type
+type PartialBinaryOp c = forall {r :: Repr} (a :: Type# r). (c a, Partial) => Biendo a
+
+type BinaryOp :: AlgebraClass -> Type
type BinaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => Biendo a
-type BinaryOpMaybe# :: MagmaClass -> Type
+type BinaryOpMaybe# :: AlgebraClass -> Type
type BinaryOpMaybe# c = forall {r :: Repr} (a :: Type# r). (c a) => a -> a -> Maybe# a
-type BinaryOpMaybe :: MagmaClass -> Type
+type BinaryOpMaybe :: AlgebraClass -> 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
+type Comm :: Endo MagmaClass
+class (c op a, HasCommutative op a) => Comm c op (a :: Type# r)
+instance forall (c :: MagmaClass) (op :: MagmaOpK) (r :: Repr) (a :: Type# r). (c op a, HasCommutative op a) => Comm c op a
--------------------------------------------------------------------------------
-- TODO: Remove Functional# superclass? We currently require it for some
-- generic definitions, but we should probably allow any representation.
--- | Semigroup
+-- | `MagmaOpK`-indexed semigroups
--
--- __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
+-- __Laws__ (in terms of `IsSemigroup`):
+-- - /`combine` is associative:/ @(x ⋄ y) ⋄ z = x ⋄ (y ⋄ z)@
+type IsSemigroupWith :: MagmaClass
+class (Functional# r) => IsSemigroupWith op (a :: Type# r) where
+ operation :: For op (Biendo a)
+
+type IsSemigroup = IsSemigroupWith Combination :: AlgebraClass
+combine, (<>), (⋄) :: BinaryOp IsSemigroup
+combine = operation Combination
(<>) = combine
(⋄) = combine
infixl 5 <>, ⋄
-type IsAddSemigroup = IsSemigroup_ Additive :: MagmaClass
-add, (+) :: forall {r :: Repr} (a :: Type# r). (IsAddSemigroup a) => Biendo a
-add = combine_ Additive
+type IsAddSemigroup = IsSemigroupWith Addition :: AlgebraClass
+add, (+) :: BinaryOp IsAddSemigroup
+add = operation Addition
(+) = add
infixl 6 +
-type IsMulSemigroup = IsSemigroup_ Multiplicative :: MagmaClass
-mul, (*) :: forall {r :: Repr} (a :: Type# r). (IsMulSemigroup a) => Biendo a
-mul = combine_ Multiplicative
+type IsMulSemigroup = IsSemigroupWith Multiplication :: AlgebraClass
+mul, (*) :: BinaryOp IsMulSemigroup
+mul = operation Multiplication
(*) = mul
infixl 7 *
--------------------------------------------------------------------------------
--- TODO: Names suck here
-
--- | Semigroup with computable left cancellation for left-cancellable elements
+-- | `MagmaOpK`-indexed semigroups with computable left cancellation for
+-- left-cancellable elements
--
--- __Laws:__
+-- __Laws__ (in terms of `PartiallyStrippableL`):
-- - /Partial left cancellation:/ if @x@ is left-cancellative, then @(x \\!) ∘ (x ⋄)@ = @identity@
--
--- We don't specify @(x \\!)@ on elements outside the image of @(x ⋄)@.
+-- We don't specify @(x \\!)@ on elements outside the image of @(x ⋄)@, nor do
+-- we specify the behavior for non-left-cancellative @x@.
--
--- Typically, monoids should also implement `PartiallyHasInverses_`
-type PartiallyCancellableL_ :: MagmaClass_
-class (IsSemigroup_ this a) => PartiallyCancellableL_ this (a :: Type# r) where
- cancelL'_ :: For this (Biendo a)
+-- Typically, monoids should also implement `PartiallyHasInverses`.
+type PartiallyCancellableL :: MagmaClass
+class (IsSemigroupWith op a) => PartiallyCancellableL op (a :: Type# r) where
+ pcancelL :: For op ((Partial) => Biendo a)
--- | Semigroup with computable right cancellation for right-cancellable elements
+-- | `MagmaOpK`-indexed semigroups with computable right cancellation for
+-- right-cancellable elements
--
--- __Laws:__
+-- __Laws__ (in terms of `PartiallyStrippableR`):
-- - /Partial right cancellation:/ if @x@ is right-cancellative, then @(//! x) ∘ (⋄ x)@ = @identity@
--
--- We don't specify @(//! x)@ on elements outside the image of @(⋄ x)@.
+-- We don't specify @(//! x)@ on elements outside the image of @(⋄ x)@, nor do
+-- we specify the behavior for non-right-cancellative @x@.
--
--- Typically, monoids should also implement `PartiallyHasInverses_`
-type PartiallyCancellableR_ :: MagmaClass_
-class (IsSemigroup_ this a) => PartiallyCancellableR_ 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, PartiallyCancellableL_ this a, PartiallyCancellableR_ this a) => PartiallyCancellable_ this (a :: Type# r)
-
-instance (Commutative_ this a, PartiallyCancellableL_ this a, PartiallyCancellableR_ this a) => PartiallyCancellable_ this (a :: Type# r)
-
-type PartiallyCancellableL = PartiallyCancellableL_ Combinative :: MagmaClass
-cancelL', (\\!) :: BinaryOp PartiallyCancellableL
-cancelL' = cancelL'_ Combinative
-(\\!) = cancelL'
+-- Typically, monoids should also implement `PartiallyHasInverses`.
+type PartiallyCancellableR :: MagmaClass
+class (IsSemigroupWith op a) => PartiallyCancellableR op (a :: Type# r) where
+ pcancelR :: For op ((Partial) => Biendo a)
+
+-- | `MagmaOpK`-indexed commutative semigroups with computable cancellation for
+-- cancellable elements
+type PartiallyCancellable :: MagmaClass
+class (HasCommutative op a, PartiallyCancellableL op a, PartiallyCancellableR op a) => PartiallyCancellable op (a :: Type# r)
+
+instance (HasCommutative op a, PartiallyCancellableL op a, PartiallyCancellableR op a) => PartiallyCancellable op (a :: Type# r)
+
+type PartiallyStrippableL = PartiallyCancellableL Combination :: AlgebraClass
+pstripL, (\\!) :: PartialBinaryOp PartiallyStrippableL
+pstripL = pcancelL Combination
+(\\!) = pstripL
infixr 5 \\!
-type PartiallyCancellableR = PartiallyCancellableR_ Combinative :: MagmaClass
-cancelR', (//!) :: BinaryOp PartiallyCancellableR
-cancelR' = cancelR'_ Combinative
-(//!) = flip cancelR'
+type PartiallyStrippableR = PartiallyCancellableR Combination :: AlgebraClass
+pstripR, (//!) :: PartialBinaryOp PartiallyStrippableR
+pstripR = pcancelR Combination
+(//!) = pstripR
infixl 5 //!
-type PartiallyCancellable = PartiallyCancellable_ Combinative :: MagmaClass
-cancel' :: BinaryOp PartiallyCancellable
-cancel' = cancelR'
+type PartiallyStrippable = PartiallyCancellable Combination :: AlgebraClass
+pstrip :: PartialBinaryOp PartiallyStrippable
+pstrip = pstripR
-type PartiallySubtractableL = PartiallyCancellableL_ Additive :: MagmaClass
-subtractL' :: BinaryOp PartiallySubtractableL
-subtractL' = cancelL'_ Additive
+type PartiallySubtractableL = PartiallyCancellableL Addition :: AlgebraClass
+psubL :: PartialBinaryOp PartiallySubtractableL
+psubL = pcancelL Addition
-type PartiallySubtractableR = PartiallyCancellableR_ Additive :: MagmaClass
-subtractR' :: BinaryOp PartiallySubtractableR
-subtractR' = cancelR'_ Additive
+type PartiallySubtractableR = PartiallyCancellableR Addition :: AlgebraClass
+psubR :: PartialBinaryOp PartiallySubtractableR
+psubR = pcancelR Addition
-- 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'
+type PartiallySubtractable = PartiallyCancellable Addition :: AlgebraClass
+psubtract, psub, (-!) :: PartialBinaryOp PartiallySubtractable
+psubtract = psubL
+psub = psubR
+(-!) = psub
infixl 6 -!
-type PartiallyDividableL = PartiallyCancellableL_ Multiplicative :: MagmaClass
-divideByL', (\!) :: BinaryOp PartiallyDividableL
-divideByL' = cancelL'_ Multiplicative
-(\!) = divideByL'
+type PartiallyDividableL = PartiallyCancellableL Multiplication :: AlgebraClass
+pdivL, (\!) :: PartialBinaryOp PartiallyDividableL
+pdivL = pcancelL Multiplication
+(\!) = pdivL
infixr 7 \!
-type PartiallyDividableR = PartiallyCancellableR_ Multiplicative :: MagmaClass
-divideByR', (/!) :: BinaryOp PartiallyDividableR
-divideByR' = cancelR'_ Multiplicative
-(/!) = flip divideByR'
+type PartiallyDividableR = PartiallyCancellableR Multiplication :: AlgebraClass
+pdivR, (/!) :: PartialBinaryOp PartiallyDividableR
+pdivR = pcancelR Multiplication
+(/!) = pdivR
infixl 7 /!
-type PartiallyDividable = PartiallyCancellable_ Multiplicative :: MagmaClass
-divideBy' :: BinaryOp PartiallyDividable
-divideBy' = divideByR'
+type PartiallyDividable = PartiallyCancellable Multiplication :: AlgebraClass
+pdiv :: PartialBinaryOp PartiallyDividable
+pdiv = pdivR
--------------------------------------------------------------------------------
--- | Semigroup with "decidable left cancellation" (i.e., decidable
--- left-cancellability and decidable images of left-combination with
+-- | `MagmaOpK`-indexed semigroups with "decidable left cancellation" (i.e.,
+-- decidable left-cancellability and decidable images of left-operation with
-- left-cancellable elements)
--
--- __Laws:__
+-- __Laws__ (in terms of `DecidablyStrippableL`):
-- - /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 DecidablyCancellableL_ :: MagmaClass_
-class (PartiallyCancellableL_ this a) => DecidablyCancellableL_ this (a :: Type# r) where
- tryCancelL_# :: For this (a -> a -> Maybe# a)
+-- Typically, monoids should also implement `DecidablyHasInverses`.
+type DecidablyCancellableL :: MagmaClass
+class (PartiallyCancellableL op a) => DecidablyCancellableL op (a :: Type# r) where
+ tryCancelL# :: For op (a -> a -> Maybe# a)
+
+tryCancelL :: forall (op :: MagmaOpK) -> BinaryOpMaybe (DecidablyCancellableL op)
+tryCancelL op = coerce (tryCancelL# op)
--- | Semigroup with "decidable right cancellation" (i.e., decidable
--- right-cancellability and decidable images of right-combination with
+-- | `MagmaOpK`-indexed semigroups with "decidable right cancellation" (i.e.,
+-- decidable right-cancellability and decidable images of right-operation with
-- right-cancellable elements)
--
--- __Laws:__
+-- __Laws__ (in terms of `DecidablyStrippableR`):
-- - /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 DecidablyCancellableR_ :: MagmaClass_
-class (PartiallyCancellableR_ this a) => DecidablyCancellableR_ 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, DecidablyCancellableL_ this a, DecidablyCancellableR_ this a) => DecidablyCancellable_ this (a :: Type# r)
-
-instance (Commutative_ this a, DecidablyCancellableL_ this a, DecidablyCancellableR_ this a) => DecidablyCancellable_ this (a :: Type# r)
-
-type DecidablyCancellableL = DecidablyCancellableL_ Combinative :: MagmaClass
-tryCancelL#, (\\?#) :: BinaryOpMaybe# DecidablyCancellableL
-tryCancelL, (\\?) :: BinaryOpMaybe DecidablyCancellableL
-tryCancelL# = tryCancelL_# Combinative
-(\\?#) = tryCancelL#
-tryCancelL = coerce tryCancelL#
-(\\?) = tryCancelL
+-- Typically, monoids should also implement `DecidablyHasInverses`.
+type DecidablyCancellableR :: MagmaClass
+class (PartiallyCancellableR op a) => DecidablyCancellableR op (a :: Type# r) where
+ tryCancelR# :: For op (a -> a -> Maybe# a)
+
+tryCancelR :: forall (op :: MagmaOpK) -> BinaryOpMaybe (DecidablyCancellableR op)
+tryCancelR op = coerce (tryCancelR# op)
+
+-- | `MagmaOpK`-indexed commutative semigroup with "decidable cancellation"
+-- (i.e., decidable cancellability and decidable images of operation with
+-- cancellable elements)
+type DecidablyCancellable :: MagmaClass
+class (HasCommutative op a, DecidablyCancellableL op a, DecidablyCancellableR op a) => DecidablyCancellable op (a :: Type# r)
+
+instance (HasCommutative op a, DecidablyCancellableL op a, DecidablyCancellableR op a) => DecidablyCancellable op (a :: Type# r)
+
+type DecidablyStrippableL = DecidablyCancellableL Combination :: AlgebraClass
+tryStripL#, (\\?#) :: BinaryOpMaybe# DecidablyStrippableL
+tryStripL, (\\?) :: BinaryOpMaybe DecidablyStrippableL
+tryStripL# = tryCancelL# Combination
+(\\?#) = tryStripL#
+tryStripL = coerce tryStripL#
+(\\?) = tryStripL
infix 5 \\?#, \\?
-type DecidablyCancellableR = DecidablyCancellableR_ Combinative :: MagmaClass
-tryCancelR#, (//?#) :: BinaryOpMaybe# DecidablyCancellableR
-tryCancelR, (//?) :: BinaryOpMaybe DecidablyCancellableR
-tryCancelR# = tryCancelR_# Combinative
-(//?#) = flip tryCancelR#
-tryCancelR = coerce tryCancelR#
-(//?) = flip tryCancelR
+type DecidablyStrippableR = DecidablyCancellableR Combination :: AlgebraClass
+tryStripR#, (//?#) :: BinaryOpMaybe# DecidablyStrippableR
+tryStripR, (//?) :: BinaryOpMaybe DecidablyStrippableR
+tryStripR# = tryCancelR# Combination
+(//?#) = tryStripR#
+tryStripR = coerce tryStripR#
+(//?) = tryStripR
infix 5 //?#, //?
-type DecidablyCancellable = DecidablyCancellable_ Combinative :: MagmaClass
-tryCancel# :: BinaryOpMaybe# DecidablyCancellable
-tryCancel :: BinaryOpMaybe DecidablyCancellable
-tryCancel# = tryCancelR#
-tryCancel = tryCancelR
-
-type DecidablySubtractableL = DecidablyCancellableL_ Additive :: MagmaClass
-trySubtractL# :: BinaryOpMaybe# DecidablySubtractableL
-trySubtractL :: BinaryOpMaybe DecidablySubtractableL
-trySubtractL# = tryCancelL_# Additive
-trySubtractL = coerce trySubtractL#
-
-type DecidablySubtractableR = DecidablyCancellableR_ Additive :: MagmaClass
-trySubtractR# :: BinaryOpMaybe# DecidablySubtractableR
-trySubtractR :: BinaryOpMaybe DecidablySubtractableR
-trySubtractR# = tryCancelR_# Additive
-trySubtractR = coerce trySubtractR#
-
-type DecidablySubtractable = DecidablyCancellable_ Additive :: MagmaClass
-trySubtract# :: BinaryOpMaybe# DecidablySubtractable
-trySubtract :: BinaryOpMaybe DecidablySubtractable
-trySubtract# = trySubtractR#
-trySubtract = trySubtractR
-
-type DecidablyDividableL = DecidablyCancellableL_ Multiplicative :: MagmaClass
-tryDivideByL#, (\?#) :: BinaryOpMaybe# DecidablyDividableL
-tryDivideByL, (\?) :: BinaryOpMaybe DecidablyDividableL
-tryDivideByL# = tryCancelL_# Multiplicative
-(\?#) = tryDivideByL#
-tryDivideByL = coerce tryDivideByL#
-(\?) = tryDivideByL
+type DecidablyStrippable = DecidablyCancellable Combination :: AlgebraClass
+tryStrip# :: BinaryOpMaybe# DecidablyStrippable
+tryStrip :: BinaryOpMaybe DecidablyStrippable
+tryStrip# = tryStripR#
+tryStrip = tryStripR
+
+type DecidablySubtractableL = DecidablyCancellableL Addition :: AlgebraClass
+trySubL# :: BinaryOpMaybe# DecidablySubtractableL
+trySubL :: BinaryOpMaybe DecidablySubtractableL
+trySubL# = tryCancelL# Addition
+trySubL = coerce trySubL#
+
+type DecidablySubtractableR = DecidablyCancellableR Addition :: AlgebraClass
+trySubR# :: BinaryOpMaybe# DecidablySubtractableR
+trySubR :: BinaryOpMaybe DecidablySubtractableR
+trySubR# = tryCancelR# Addition
+trySubR = coerce trySubR#
+
+type DecidablySubtractable = DecidablyCancellable Addition :: AlgebraClass
+trySub#, (-?#) :: BinaryOpMaybe# DecidablySubtractable
+trySub, (-?) :: BinaryOpMaybe DecidablySubtractable
+trySub# = trySubR#
+(-?#) = trySub#
+trySub = trySubR
+(-?) = trySub
+infix 6 -?#, -?
+
+type DecidablyDividableL = DecidablyCancellableL Multiplication :: AlgebraClass
+tryDivL#, (\?#) :: BinaryOpMaybe# DecidablyDividableL
+tryDivL, (\?) :: BinaryOpMaybe DecidablyDividableL
+tryDivL# = tryCancelL# Multiplication
+(\?#) = tryDivL#
+tryDivL = coerce tryDivL#
+(\?) = tryDivL
infix 7 \?#, \?
-type DecidablyDividableR = DecidablyCancellableR_ Multiplicative :: MagmaClass
-tryDivideByR#, (/?#) :: BinaryOpMaybe# DecidablyDividableR
-tryDivideByR, (/?) :: BinaryOpMaybe DecidablyDividableR
-tryDivideByR# = tryCancelR_# Multiplicative
-(/?#) = flip tryDivideByR#
-tryDivideByR = coerce tryDivideByR#
-(/?) = flip tryDivideByR
+type DecidablyDividableR = DecidablyCancellableR Multiplication :: AlgebraClass
+tryDivR#, (/?#) :: BinaryOpMaybe# DecidablyDividableR
+tryDivR, (/?) :: BinaryOpMaybe DecidablyDividableR
+tryDivR# = tryCancelR# Multiplication
+(/?#) = tryDivR#
+tryDivR = coerce tryDivR#
+(/?) = tryDivR
infix 7 /?#, /?
-type DecidablyDividable = DecidablyCancellable_ Multiplicative :: MagmaClass
-tryDivideBy# :: BinaryOpMaybe# DecidablyDividable
-tryDivideBy :: BinaryOpMaybe DecidablyDividable
-tryDivideBy# = tryDivideByR#
-tryDivideBy = tryDivideByR
+type DecidablyDividable = DecidablyCancellable Multiplication :: AlgebraClass
+tryDiv# :: BinaryOpMaybe# DecidablyDividable
+tryDiv :: BinaryOpMaybe DecidablyDividable
+tryDiv# = tryDivR#
+tryDiv = tryDivR
--------------------------------------------------------------------------------
--- | Monoid
+-- | `MagmaOpK`-indexed monoids
--
--- __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
+-- __Laws__ (in terms of `IsMonoid`):
+-- - /@nil@ is a (left and right) identity element:/ @nil ⋄ x = x = x ⋄ nil@
+type IsMonoidWith :: MagmaClass
+class (IsSemigroupWith op a) => IsMonoidWith op (a :: Type# r) where
+ neutral :: For op a
-type IsMonoid = IsMonoid_ Combinative :: MagmaClass
-neutral :: forall {r :: Repr} (a :: Type# r). (IsMonoid a) => a
-neutral = neutral_ Combinative
+type IsMonoid = IsMonoidWith Combination :: AlgebraClass
+nil :: NullaryOp IsMonoid
+nil = neutral Combination
-type IsAddMonoid = IsMonoid_ Additive :: MagmaClass
-zero :: forall {r :: Repr} (a :: Type# r). (IsAddMonoid a) => a
-zero = neutral_ Additive
+type IsAddMonoid = IsMonoidWith Addition :: AlgebraClass
+zero :: NullaryOp IsAddMonoid
+zero = neutral Addition
-type IsMulMonoid = IsMonoid_ Multiplicative :: MagmaClass
-one :: forall {r :: Repr} (a :: Type# r). (IsMulMonoid a) => a
-one = neutral_ Multiplicative
+type IsMulMonoid = IsMonoidWith Multiplication :: AlgebraClass
+one :: NullaryOp IsMulMonoid
+one = neutral Multiplication
--------------------------------------------------------------------------------
-- 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
+-- | `MagmaOpK`-indexed monoids with computable inverses for invertible elements
--
--- __Laws:__
--- - /Partial inversion:/ if @x@ has inverse @y@, then @invert' x = y@
+-- __Laws__ (in terms of `PartiallyHasUndos`):
+-- - /Partial inversion:/ if @x@ has inverse @y@, then @pundo 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)
+-- We don't specify @pundo@ on non-invertible elements.
+type PartiallyHasInverses :: MagmaClass
+class (IsMonoidWith op a) => PartiallyHasInverses op (a :: Type# r) where
+ pinvert :: For op ((Partial) => Endo a)
-type PartiallyHasInverses = PartiallyHasInverses_ Combinative :: MagmaClass
-invert' :: UnaryOp PartiallyHasInverses
-invert' = invert'_ Combinative
+type PartiallyHasUndos = PartiallyHasInverses Combination :: AlgebraClass
+pundo :: PartialUnaryOp PartiallyHasUndos
+pundo = pinvert Combination
-type PartiallyHasNegations = PartiallyHasInverses_ Additive :: MagmaClass
-negate' :: UnaryOp PartiallyHasNegations
-negate' = invert'_ Additive
+type PartiallyHasNegations = PartiallyHasInverses Addition :: AlgebraClass
+pnegate :: PartialUnaryOp PartiallyHasNegations
+pnegate = pinvert Addition
-type PartiallyHasReciprocals = PartiallyHasInverses_ Multiplicative :: MagmaClass
-recip' :: UnaryOp PartiallyHasReciprocals
-recip' = invert'_ Multiplicative
+type PartiallyHasReciprocals = PartiallyHasInverses Multiplication :: AlgebraClass
+precip :: PartialUnaryOp PartiallyHasReciprocals
+precip = pinvert Multiplication
--------------------------------------------------------------------------------
--- | Monoid with decidable invertibility and computable inverses for invertible
--- elements
+-- | `MagmaOpK`-indexed monoids 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
+-- __Laws__ (in terms of `DecidablyHasUndos`):
+-- - /Decidable inversion:/ if @x@ has inverse @y@, then @tryUndo x@ =
+-- @Just y@; otherwise, @tryUndo x = Nothing@
+type DecidablyHasInverses :: MagmaClass
+class (PartiallyHasInverses op a) => DecidablyHasInverses op (a :: Type# r) where
+ tryInvert# :: For op (a -> Maybe# a)
+
+tryInvert :: forall (op :: MagmaOpK) -> UnaryOpMaybe (DecidablyHasInverses op)
+tryInvert op = coerce (tryInvert# op)
+
+type DecidablyHasUndos = DecidablyHasInverses Combination :: AlgebraClass
+tryUndo# :: UnaryOpMaybe# DecidablyHasUndos
+tryUndo :: UnaryOpMaybe DecidablyHasUndos
+tryUndo# = tryInvert# Combination
+tryUndo = coerce tryUndo#
+
+type DecidablyHasNegations = DecidablyHasInverses Addition :: AlgebraClass
tryNegate# :: UnaryOpMaybe# DecidablyHasNegations
tryNegate :: UnaryOpMaybe DecidablyHasNegations
-tryNegate# = tryInvert_# Additive
+tryNegate# = tryInvert# Addition
tryNegate = coerce tryNegate#
-type DecidablyHasReciprocals = DecidablyHasInverses_ Multiplicative :: MagmaClass
+type DecidablyHasReciprocals = DecidablyHasInverses Multiplication :: AlgebraClass
tryRecip# :: UnaryOpMaybe# DecidablyHasReciprocals
tryRecip :: UnaryOpMaybe DecidablyHasReciprocals
-tryRecip# = tryInvert_# Multiplicative
+tryRecip# = tryInvert# Multiplication
tryRecip = coerce tryRecip#
--------------------------------------------------------------------------------
--- | Group
+-- | `MagmaOpK`-indexed groups
--
--- __Laws:__
--- - /Every element is invertible:/ @isJust (tryInvert x)@ = @True@
-type IsGroup_ :: MagmaClass_
-class (DecidablyHasInverses_ this a, DecidablyCancellableL_ this a, DecidablyCancellableR_ 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'
+-- __Laws__ (in terms of `IsGroup`):
+-- - /Every element is invertible:/ @isJust (tryUndo x)@ = @True@
+type IsGroupWith :: MagmaClass
+class (DecidablyHasInverses op a, DecidablyCancellableL op a, DecidablyCancellableR op a) => IsGroupWith op (a :: Type# r)
+
+cancelL, cancelR :: forall (op :: MagmaOpK) -> BinaryOp (IsGroupWith op)
+invert :: forall (op :: MagmaOpK) -> UnaryOp (IsGroupWith op)
+cancelL op = unsafe_partial (pcancelL op)
+cancelR op = unsafe_partial (pcancelR op)
+invert op = unsafe_partial (pinvert op)
+
+type IsGroup = IsGroupWith Combination :: AlgebraClass
+stripL, (\\), stripR, (//) :: BinaryOp IsGroup
+undo :: UnaryOp IsGroup
+stripL = unsafe_partial pstripL
+(\\) = unsafe_partial (\\!)
+stripR = unsafe_partial pstripR
+(//) = unsafe_partial (//!)
+undo = unsafe_partial pundo
infixr 5 \\
infixl 5 //
-type IsAddGroup = IsGroup_ Additive :: MagmaClass
-subtractL, subtractR :: BinaryOp IsAddGroup
+type IsAddGroup = IsGroupWith Addition :: AlgebraClass
+subL, subR :: BinaryOp IsAddGroup
subtract, sub, (-) :: BinaryOp IsCommAddGroup
negate :: UnaryOp IsAddGroup
-subtractL = subtractL'
-subtractR = subtractR'
-subtract = subtract'
-sub = sub'
-(-) = (-!)
-negate = negate'
+subL = unsafe_partial psubL
+subR = unsafe_partial psubR
+subtract = unsafe_partial psubtract
+sub = unsafe_partial psub
+(-) = unsafe_partial (-!)
+negate = unsafe_partial pnegate
infixl 6 -
-type IsMulGroup = IsGroup_ Multiplicative :: MagmaClass
-divideByL, divideByR, (/) :: BinaryOp IsMulGroup -- NOTE: (\) is reserved in Haskell :(
-divideBy :: BinaryOp IsCommMulGroup
+type IsMulGroup = IsGroupWith Multiplication :: AlgebraClass
+divL, divR, (/) :: BinaryOp IsMulGroup -- NOTE: (\) is reserved in Haskell :(
+div :: BinaryOp IsCommMulGroup
recip :: UnaryOp IsMulGroup
-divideByL = divideByL'
-divideByR = divideByR'
-(/) = (/!)
-divideBy = divideBy'
-recip = recip'
+divL = unsafe_partial pdivL
+divR = unsafe_partial pdivR
+(/) = unsafe_partial (/!)
+div = unsafe_partial pdiv
+recip = unsafe_partial precip
infixl 7 /
--------------------------------------------------------------------------------
--- | Commutative semigroup
+-- | Commutative semigroups
--
--- __Laws:__
+-- __Laws__ (in terms of `IsCommSemigroup`):
-- - /@combine@ is commutative:/ @x ⋄ y = y ⋄ x@
-type Commutative_ :: MagmaClass_
-class (IsSemigroup_ this a) => Commutative_ this (a :: Type# r)
+type HasCommutative :: MagmaClass
+class (IsSemigroupWith op a) => HasCommutative op (a :: Type# r)
-type Commutative = Commutative_ Combinative :: MagmaClass
-type AddCommutative = Commutative_ Additive :: MagmaClass
-type MulCommutative = Commutative_ Multiplicative :: MagmaClass
+type Commutative = HasCommutative Combination :: AlgebraClass
+type AddCommutative = HasCommutative Addition :: AlgebraClass
+type MulCommutative = HasCommutative Multiplication :: AlgebraClass
-type IsCommSemigroup = Comm IsSemigroup_ Combinative :: MagmaClass
-type IsCommAddSemigroup = Comm IsSemigroup_ Additive :: MagmaClass
-type IsCommMulSemigroup = Comm IsSemigroup_ Multiplicative :: MagmaClass
+type IsCommSemigroup = Comm IsSemigroupWith Combination :: AlgebraClass
+type IsCommAddSemigroup = Comm IsSemigroupWith Addition :: AlgebraClass
+type IsCommMulSemigroup = Comm IsSemigroupWith Multiplication :: AlgebraClass
-type IsCommMonoid = Comm IsMonoid_ Combinative :: MagmaClass
-type IsCommAddMonoid = Comm IsMonoid_ Additive :: MagmaClass
-type IsCommMulMonoid = Comm IsMonoid_ Multiplicative :: MagmaClass
+type IsCommMonoid = Comm IsMonoidWith Combination :: AlgebraClass
+type IsCommAddMonoid = Comm IsMonoidWith Addition :: AlgebraClass
+type IsCommMulMonoid = Comm IsMonoidWith Multiplication :: AlgebraClass
-type IsCommGroup = Comm IsGroup_ Combinative :: MagmaClass
-type IsCommAddGroup = Comm IsGroup_ Additive :: MagmaClass
-type IsCommMulGroup = Comm IsGroup_ Multiplicative :: MagmaClass
+type IsCommGroup = Comm IsGroupWith Combination :: AlgebraClass
+type IsCommAddGroup = Comm IsGroupWith Addition :: AlgebraClass
+type IsCommMulGroup = Comm IsGroupWith Multiplication :: AlgebraClass
--------------------------------------------------------------------------------
@@ -633,24 +676,24 @@ type IsCommMulGroup = Comm IsGroup_ Multiplicative :: MagmaClass
-- TODO: DecidableZero for decidable division rings (and fields)?
-type IsSemiring :: MagmaClass
+type IsSemiring :: AlgebraClass
class (IsCommAddMonoid a, IsMulMonoid a) => IsSemiring (a :: Type# r)
-type IsCommSemiring :: MagmaClass
+type IsCommSemiring :: AlgebraClass
class (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r)
instance (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r)
-type IsRing :: MagmaClass
+type IsRing :: AlgebraClass
class (IsSemiring a, IsAddGroup a) => IsRing (a :: Type# r)
-type IsCommRing :: MagmaClass
+type IsCommRing :: AlgebraClass
class (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r)
instance (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r)
-type IsDivisionRing :: MagmaClass
+type IsDivisionRing :: AlgebraClass
class (IsRing a, PartiallyDividableL a, PartiallyDividableR a, PartiallyHasReciprocals a) => IsDivisionRing a
-type IsField :: MagmaClass
+type IsField :: AlgebraClass
class (IsDivisionRing a, MulCommutative a) => IsField a
instance (IsDivisionRing a, MulCommutative a) => IsField a
@@ -662,23 +705,23 @@ 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) => PartiallyCancellableL_ Additive (BaseInterop a) where cancelL'_ _ = coerce Base.subtract
-instance (Base.Num a) => DecidablyCancellableL_ Additive (BaseInterop a) where tryCancelL_# _ = coerce $ Just .* Base.subtract
-instance (Base.Num a) => PartiallyCancellableR_ Additive (BaseInterop a) where cancelR'_ _ = coerce Base.subtract
-instance (Base.Num a) => DecidablyCancellableR_ Additive (BaseInterop a) where tryCancelR_# _ = coerce $ Just .* Base.subtract
-instance (Base.Num a) => IsMonoid_ Additive (BaseInterop a) where neutral_ _ = coerce baseZero
-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) => 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) => IsSemigroupWith Addition (BaseInterop a) where operation _ = coerce (Base.+)
+instance (Base.Num a) => PartiallyCancellableL Addition (BaseInterop a) where pcancelL _ = coerce Base.subtract
+instance (Base.Num a) => DecidablyCancellableL Addition (BaseInterop a) where tryCancelL# _ = coerce $ Just .* Base.subtract
+instance (Base.Num a) => PartiallyCancellableR Addition (BaseInterop a) where pcancelR _ = coerce (Base.-)
+instance (Base.Num a) => DecidablyCancellableR Addition (BaseInterop a) where tryCancelR# _ = coerce $ Just .* (Base.-)
+instance (Base.Num a) => IsMonoidWith Addition (BaseInterop a) where neutral _ = coerce baseZero
+instance (Base.Num a) => PartiallyHasInverses Addition (BaseInterop a) where pinvert _ = coerce Base.negate
+instance (Base.Num a) => DecidablyHasInverses Addition (BaseInterop a) where tryInvert# _ = coerce $ Just . Base.negate
+instance (Base.Num a) => IsGroupWith Addition (BaseInterop a)
+instance (Base.Num a) => HasCommutative Addition (BaseInterop a)
+instance (Base.Num a) => IsSemigroupWith Multiplication (BaseInterop a) where operation _ = coerce (Base.*)
+instance (Base.Num a) => IsMonoidWith Multiplication (BaseInterop a) where neutral _ = coerce baseOne
instance (Base.Num a) => IsSemiring (BaseInterop a)
instance (Base.Num a) => IsRing (BaseInterop a)
-instance (Base.Fractional a) => PartiallyCancellableL_ Multiplicative (BaseInterop a) where cancelL'_ _ = coerce \x y -> Base.recip x Base.* y
-instance (Base.Fractional a) => PartiallyCancellableR_ 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) => PartiallyCancellableL Multiplication (BaseInterop a) where pcancelL _ = coerce \x y -> Base.recip x Base.* y
+instance (Base.Fractional a) => PartiallyCancellableR Multiplication (BaseInterop a) where pcancelR _ = coerce (Base./)
+instance (Base.Fractional a) => PartiallyHasInverses Multiplication (BaseInterop a) where pinvert _ = coerce Base.recip
instance (Base.Fractional a) => IsDivisionRing (BaseInterop a)
--------------------------------------------------------------------------------
@@ -689,67 +732,67 @@ 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 PartiallyCancellableL_ Additive Natural
-instance DecidablyCancellableL_ Additive Natural where tryCancelL_# _ = coerce $ flip Base.minusNaturalMaybe
-deriving via BaseInterop Natural instance PartiallyCancellableR_ Additive Natural
-instance DecidablyCancellableR_ 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 IsSemigroupWith Addition Natural
+deriving via BaseInterop Natural instance PartiallyCancellableL Addition Natural
+instance DecidablyCancellableL Addition Natural where tryCancelL# _ = coerce $ flip Base.minusNaturalMaybe
+deriving via BaseInterop Natural instance PartiallyCancellableR Addition Natural
+instance DecidablyCancellableR Addition Natural where tryCancelR# _ = coerce Base.minusNaturalMaybe
+deriving via BaseInterop Natural instance IsMonoidWith Addition Natural
+deriving via BaseInterop Natural instance HasCommutative Addition Natural
+deriving via BaseInterop Natural instance IsSemigroupWith Multiplication Natural
+deriving via BaseInterop Natural instance IsMonoidWith Multiplication Natural
+instance HasCommutative Multiplication Natural
deriving via BaseInterop Natural instance IsSemiring Natural
-deriving via BaseInterop Integer instance IsSemigroup_ Additive Integer
-deriving via BaseInterop Integer instance PartiallyCancellableL_ Additive Integer
-deriving via BaseInterop Integer instance DecidablyCancellableL_ Additive Integer
-deriving via BaseInterop Integer instance PartiallyCancellableR_ Additive Integer
-deriving via BaseInterop Integer instance DecidablyCancellableR_ 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 IsSemigroupWith Addition Integer
+deriving via BaseInterop Integer instance PartiallyCancellableL Addition Integer
+deriving via BaseInterop Integer instance DecidablyCancellableL Addition Integer
+deriving via BaseInterop Integer instance PartiallyCancellableR Addition Integer
+deriving via BaseInterop Integer instance DecidablyCancellableR Addition Integer
+deriving via BaseInterop Integer instance IsMonoidWith Addition Integer
+deriving via BaseInterop Integer instance PartiallyHasInverses Addition Integer
+deriving via BaseInterop Integer instance DecidablyHasInverses Addition Integer
+deriving via BaseInterop Integer instance IsGroupWith Addition Integer
+deriving via BaseInterop Integer instance HasCommutative Addition Integer
+deriving via BaseInterop Integer instance IsSemigroupWith Multiplication Integer
+deriving via BaseInterop Integer instance IsMonoidWith Multiplication Integer
+instance HasCommutative Multiplication 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 PartiallyCancellableL_ Additive Rational
-deriving via BaseInterop Rational instance DecidablyCancellableL_ Additive Rational
-deriving via BaseInterop Rational instance PartiallyCancellableR_ Additive Rational
-deriving via BaseInterop Rational instance DecidablyCancellableR_ 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 IsSemigroupWith Addition Rational
+deriving via BaseInterop Rational instance PartiallyCancellableL Addition Rational
+deriving via BaseInterop Rational instance DecidablyCancellableL Addition Rational
+deriving via BaseInterop Rational instance PartiallyCancellableR Addition Rational
+deriving via BaseInterop Rational instance DecidablyCancellableR Addition Rational
+deriving via BaseInterop Rational instance IsMonoidWith Addition Rational
+deriving via BaseInterop Rational instance PartiallyHasInverses Addition Rational
+deriving via BaseInterop Rational instance DecidablyHasInverses Addition Rational
+deriving via BaseInterop Rational instance IsGroupWith Addition Rational
+deriving via BaseInterop Rational instance HasCommutative Addition Rational
+deriving via BaseInterop Rational instance IsSemigroupWith Multiplication Rational
+deriving via BaseInterop Rational instance IsMonoidWith Multiplication Rational
+instance HasCommutative Multiplication Rational
deriving via BaseInterop Rational instance IsSemiring Rational
deriving via BaseInterop Rational instance IsRing Rational
-deriving via BaseInterop Rational instance PartiallyCancellableL_ Multiplicative Rational
-instance DecidablyCancellableL_ Multiplicative Rational where tryCancelL_# _ = coerce $ flip baseDivNonZero
-deriving via BaseInterop Rational instance PartiallyCancellableR_ Multiplicative Rational
-instance DecidablyCancellableR_ 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 PartiallyCancellableL Multiplication Rational
+instance DecidablyCancellableL Multiplication Rational where tryCancelL# _ = coerce $ flip baseDivNonZero
+deriving via BaseInterop Rational instance PartiallyCancellableR Multiplication Rational
+instance DecidablyCancellableR Multiplication Rational where tryCancelR# _ = coerce baseDivNonZero
+deriving via BaseInterop Rational instance PartiallyHasInverses Multiplication Rational
+instance DecidablyHasInverses Multiplication 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 (PartiallyCancellableL_ this a) => PartiallyCancellableL_ this (r -> a) where cancelL'_ _ = Base.liftA2 (cancelL'_ this)
-instance (PartiallyCancellableR_ this a) => PartiallyCancellableR_ 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) => DecidablyCancellableL_ this (r -> a) where tryCancelL_# _ = just# .* cancelL'_ this
-instance (IsGroup_ this a) => DecidablyCancellableR_ 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 (IsSemigroupWith op a) => IsSemigroupWith op (r -> a) where operation _ = Base.liftA2 (operation op)
+instance (PartiallyCancellableL op a) => PartiallyCancellableL op (r -> a) where pcancelL _ = Base.liftA2 (pcancelL op)
+instance (PartiallyCancellableR op a) => PartiallyCancellableR op (r -> a) where pcancelR _ = Base.liftA2 (pcancelR op)
+instance (IsMonoidWith op a) => IsMonoidWith op (r -> a) where neutral _ = Base.const (neutral op)
+instance (PartiallyHasInverses op a) => PartiallyHasInverses op (r -> a) where pinvert _ = Base.fmap (pinvert op)
+instance (IsGroupWith op a) => DecidablyCancellableL op (r -> a) where tryCancelL# _ = just# .* cancelL op
+instance (IsGroupWith op a) => DecidablyCancellableR op (r -> a) where tryCancelR# _ = just# .* cancelR op
+instance (IsGroupWith op a) => DecidablyHasInverses op (r -> a) where tryInvert# _ = just# . invert op
+instance (IsGroupWith op a) => IsGroupWith op (r -> a)
+instance (HasCommutative op a) => HasCommutative op (r -> a)
instance (IsSemiring a) => IsSemiring (r -> a)
instance (IsRing a) => IsRing (r -> a)
