commit b40f468c8ea5209a59a422eb9ecb9ab26f92794f
parent e6a72b4809b29d1a2dba3d5766001ef2b3df7e41
Author: Robert Russell <robert@rr3.xyz>
Date: Fri, 16 Oct 2026 10:14:45 -0700
Algebra.Magma: add fromInteger
Diffstat:
1 file changed, 31 insertions(+), 8 deletions(-)
diff --git a/src/Lude/Algebra/Magma.hs b/src/Lude/Algebra/Magma.hs
@@ -173,23 +173,29 @@ module Lude.Algebra.Magma (
IsCommRing,
IsDivisionRing,
IsField,
+ fromInteger,
) where
import Data.Coerce
import Data.Text (Text)
import Data.Text qualified as Text
-import Numeric.Natural (Natural)
import Numeric.Natural qualified as Base
-import Prelude (Integer, Rational)
+import Prelude (Rational)
import Prelude qualified as Base
import Lude.Algebra.Category.Core
+import Lude.Error
import Lude.Function
import Lude.Haskell
+import Lude.Integer
import Lude.Maybe
+import Lude.Natural
-- TODO: Break this up.
+-- TODO: Generally make this depend less-directly on base (i.e., re-export more
+-- from Lude.Haskell)
+
-- 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
@@ -680,14 +686,23 @@ type IsCommMulGroup = Comm IsGroupWith Multiplication :: AlgebraClass
-- TODO: DecidableZero for decidable division rings (and fields)?
type IsSemiring :: AlgebraClass
-class (IsCommAddMonoid a, IsMulMonoid a) => IsSemiring (a :: Type# r)
+class (IsCommAddMonoid a, IsMulMonoid a) => IsSemiring (a :: Type# r) where
+ ofNatural :: Natural -> a
+ ofNatural = \case
+ NaturalZero -> zero
+ NaturalSucc n -> app2# (+) one (ofNatural n)
type IsCommSemiring :: AlgebraClass
class (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r)
instance (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r)
type IsRing :: AlgebraClass
-class (IsSemiring a, IsAddGroup a) => IsRing (a :: Type# r)
+class (IsSemiring a, IsAddGroup a) => IsRing (a :: Type# r) where
+ ofInteger :: Integer -> a
+ ofInteger = \case
+ IntegerNegSucc n -> negate $# ofNatural (NaturalSucc n)
+ IntegerZero -> zero
+ IntegerPosSucc n -> ofNatural (NaturalSucc n)
type IsCommRing :: AlgebraClass
class (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r)
@@ -700,6 +715,14 @@ type IsField :: AlgebraClass
class (IsDivisionRing a, MulCommutative a) => IsField a
instance (IsDivisionRing a, MulCommutative a) => IsField a
+-- TODO: This probably doesn't belong here.
+fromInteger :: forall {r :: Repr} (a :: Type# r). (IsSemiring a) => Integer -> a
+fromInteger = \case
+ IntegerNegSucc _ -> panic "fromInteger on negative integer; disable NegativeLiterals"
+ IntegerZero -> ofNatural NaturalZero
+ IntegerPosSucc n -> ofNatural (NaturalSucc n)
+{-# INLINE fromInteger #-}
+
--------------------------------------------------------------------------------
baseZero :: (Base.Num a) => a
@@ -720,8 +743,8 @@ 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.Num a) => IsSemiring (BaseInterop a) where ofNatural = coerce Base.fromIntegral
+instance (Base.Num a) => IsRing (BaseInterop a) where ofInteger = coerce Base.fromInteger
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
@@ -800,8 +823,8 @@ instance (IsGroupWith op a) => DecidablyCancellableR op (r -> a) where tryCancel
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)
+instance (IsSemiring a) => IsSemiring (r -> a) where ofNatural = Base.const . ofNatural
+instance (IsRing a) => IsRing (r -> a) where ofInteger = Base.const . ofInteger
deriving via BaseInterop Text instance IsSemigroupWith Combination Text
instance PartiallyCancellableL Combination Text where pcancelL _ p x = Text.stripPrefix p x ?? x
