Magma.hs (31529B)
1 {-# LANGUAGE UndecidableInstances #-} 2 {-# LANGUAGE UndecidableSuperClasses #-} 3 4 module Lude.Algebra.Magma ( 5 -- * Magma operations 6 MagmaOpK, 7 Combination, 8 Addition, 9 Multiplication, 10 11 -- * Semigroups 12 IsSemigroupWith (..), 13 IsSemigroup, 14 combine, 15 (<>), 16 (⋄), 17 IsAddSemigroup, 18 add, 19 (+), 20 IsMulSemigroup, 21 mul, 22 (*), 23 24 -- * Partial cancellation 25 PartiallyCancellableL (..), 26 PartiallyCancellableR (..), 27 PartiallyCancellable, 28 PartiallyStrippableL, 29 pstripL, 30 (\\!), 31 PartiallyStrippableR, 32 pstripR, 33 (//!), 34 PartiallyStrippable, 35 pstrip, 36 PartiallySubtractableL, 37 psubL, 38 PartiallySubtractableR, 39 psubR, 40 PartiallySubtractable, 41 psubtract, 42 psub, 43 (-!), 44 PartiallyDividableL, 45 pdivL, 46 (\!), 47 PartiallyDividableR, 48 pdivR, 49 (/!), 50 PartiallyDividable, 51 pdiv, 52 53 -- * Decidable cancellation 54 DecidablyCancellableL (..), 55 tryCancelL, 56 DecidablyCancellableR (..), 57 tryCancelR, 58 DecidablyCancellable, 59 DecidablyStrippableL, 60 tryStripL#, 61 (\\?#), 62 tryStripL, 63 (\\?), 64 DecidablyStrippableR, 65 tryStripR#, 66 (//?#), 67 tryStripR, 68 (//?), 69 DecidablyStrippable, 70 tryStrip#, 71 tryStrip, 72 DecidablySubtractableL, 73 trySubL#, 74 trySubL, 75 DecidablySubtractableR, 76 trySubR#, 77 trySubR, 78 DecidablySubtractable, 79 trySub#, 80 (-?#), 81 trySub, 82 (-?), 83 DecidablyDividableL, 84 tryDivL#, 85 (\?#), 86 tryDivL, 87 (\?), 88 DecidablyDividableR, 89 tryDivR#, 90 (/?#), 91 tryDivR, 92 (/?), 93 DecidablyDividable, 94 tryDiv#, 95 tryDiv, 96 97 -- * Monoids 98 IsMonoidWith (..), 99 IsMonoid, 100 nil, 101 IsAddMonoid, 102 zero, 103 IsMulMonoid, 104 one, 105 106 -- * Partial inverses 107 PartiallyHasInverses (..), 108 PartiallyHasUndos, 109 pundo, 110 PartiallyHasNegations, 111 pnegate, 112 PartiallyHasReciprocals, 113 precip, 114 115 -- * Decidable inverses 116 DecidablyHasInverses (..), 117 tryInvert, 118 DecidablyHasUndos, 119 tryUndo#, 120 tryUndo, 121 DecidablyHasNegations, 122 tryNegate#, 123 tryNegate, 124 DecidablyHasReciprocals, 125 tryRecip#, 126 tryRecip, 127 128 -- * Groups 129 IsGroupWith, 130 cancelL, 131 cancelR, 132 invert, 133 IsGroup, 134 stripL, 135 -- TODO: Rename the conflicting (\\) 136 -- (\\), 137 stripR, 138 (//), 139 undo, 140 IsAddGroup, 141 subL, 142 subR, 143 subtract, 144 sub, 145 (-), 146 negate, 147 IsMulGroup, 148 divL, 149 divR, 150 (/), 151 div, 152 recip, 153 154 -- * Commutativity 155 HasCommutative, 156 Commutative, 157 AddCommutative, 158 MulCommutative, 159 IsCommSemigroup, 160 IsCommAddSemigroup, 161 IsCommMulSemigroup, 162 IsCommMonoid, 163 IsCommAddMonoid, 164 IsCommMulMonoid, 165 IsCommGroup, 166 IsCommAddGroup, 167 IsCommMulGroup, 168 169 -- * Rings 170 IsSemiring, 171 IsCommSemiring, 172 IsRing, 173 IsCommRing, 174 IsDivisionRing, 175 IsField, 176 fromInteger, 177 ) where 178 179 import Data.Coerce 180 import Data.Text (Text) 181 import Data.Text qualified as Text 182 import Numeric.Natural qualified as Base 183 import Prelude (Rational) 184 import Prelude qualified as Base 185 186 import Lude.Algebra.Category.Core 187 import Lude.Error 188 import Lude.Function 189 import Lude.Haskell 190 import Lude.Integer 191 import Lude.Maybe 192 import Lude.Natural 193 194 -- TODO: Break this up. 195 196 -- TODO: Generally make this depend less-directly on base (i.e., re-export more 197 -- from Lude.Haskell) 198 199 -- TODO: We should somehow connect these to the categorical abstractions, so 200 -- that we don't have two abstraction islands. E.g., maybe all these should be 201 -- required to form an Eilenberg-Moore algebra (except the truely 202 -- "non-algebraic" ones, like fields). 203 204 -- TODO: Should the initial rig/ring maps (out of Natural/Integer) use 205 -- the categorical machinery for initial objects? 206 207 -- TODO: newtype to view X as X-oid with one object, and vice versa. 208 209 -- TODO: Should addition be commutative always? It conventionally is. 210 211 -- TODO: Torsors 212 213 -- TODO: Modular integers with arbitrary modulus (requires passing around 214 -- modulus; see Oleg paper) 215 216 -- TODO: Invertible/Unit type (newtype wrapper or pair) for the group of units, 217 -- the non-oidified version of Iso 218 219 -- TODO: Decidable sign for ordered ring-like things 220 221 -- TODO: Left- and right- actions 222 223 -- TODO: Localization / field of fractions / Ratio 224 225 -- TODO: Euclidean div/mod 226 227 -- TODO: 228 -- type Exp :: forall {r :: Repr}. Type# r -> Type# r 229 -- newtype Exp a = MkExp a 230 -- type Log :: forall {r :: Repr}. Type# r -> Type# r 231 -- newtype Log a = MkLog a 232 233 -------------------------------------------------------------------------------- 234 235 data MagmaOpB :: Brand 236 237 -- | The `OpenKind` of magma operations 238 -- 239 -- We index `MagmaClass`es by `MagmaOpK` to enable working generically over 240 -- magmas that differ only in notation. 241 -- 242 -- Lude has three standard magma operations: 243 -- `Combination` (generic), `Addition`, and `Multiplication`. 244 type MagmaOpK = OpenKind MagmaOpB 245 246 data Combination :: MagmaOpK 247 data Addition :: MagmaOpK 248 data Multiplication :: MagmaOpK 249 250 -------------------------------------------------------------------------------- 251 -- Private Util 252 253 type AlgebraClass :: Kind 254 type AlgebraClass = forall {r :: Repr}. Type# r -> Constraint 255 256 type MagmaClass :: Kind 257 type MagmaClass = MagmaOpK -> AlgebraClass 258 259 type NullaryOp :: AlgebraClass -> Type 260 type NullaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => a 261 262 type PartialUnaryOp :: AlgebraClass -> Type 263 type PartialUnaryOp c = forall {r :: Repr} (a :: Type# r). (c a, Partial) => Endo a 264 265 type UnaryOp :: AlgebraClass -> Type 266 type UnaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => Endo a 267 268 type UnaryOpMaybe# :: AlgebraClass -> Type 269 type UnaryOpMaybe# c = forall {r :: Repr} (a :: Type# r). (c a) => a -> Maybe# a 270 271 type UnaryOpMaybe :: AlgebraClass -> Type 272 type UnaryOpMaybe c = forall (a :: Type). (c a) => a -> Maybe a 273 274 type PartialBinaryOp :: AlgebraClass -> Type 275 type PartialBinaryOp c = forall {r :: Repr} (a :: Type# r). (c a, Partial) => Biendo a 276 277 type BinaryOp :: AlgebraClass -> Type 278 type BinaryOp c = forall {r :: Repr} (a :: Type# r). (c a) => Biendo a 279 280 type BinaryOpMaybe# :: AlgebraClass -> Type 281 type BinaryOpMaybe# c = forall {r :: Repr} (a :: Type# r). (c a) => a -> a -> Maybe# a 282 283 type BinaryOpMaybe :: AlgebraClass -> Type 284 type BinaryOpMaybe c = forall (a :: Type). (c a) => a -> a -> Maybe a 285 286 type Comm :: Endo MagmaClass 287 class (c op a, HasCommutative op a) => Comm c op (a :: Type# r) 288 instance forall (c :: MagmaClass) (op :: MagmaOpK) (r :: Repr) (a :: Type# r). (c op a, HasCommutative op a) => Comm c op a 289 290 -------------------------------------------------------------------------------- 291 292 -- TODO: Remove Functional# superclass? We currently require it for some 293 -- generic definitions, but we should probably allow any representation. 294 295 -- | `MagmaOpK`-indexed semigroups 296 -- 297 -- __Laws__ (in terms of `IsSemigroup`): 298 -- - /`combine` is associative:/ @(x ⋄ y) ⋄ z = x ⋄ (y ⋄ z)@ 299 type IsSemigroupWith :: MagmaClass 300 class (Functional# r) => IsSemigroupWith op (a :: Type# r) where 301 operation :: For op (Biendo a) 302 303 type IsSemigroup = IsSemigroupWith Combination :: AlgebraClass 304 combine, (<>), (⋄) :: BinaryOp IsSemigroup 305 combine = operation Combination 306 (<>) = combine 307 (⋄) = combine 308 infixl 5 <>, ⋄ 309 310 type IsAddSemigroup = IsSemigroupWith Addition :: AlgebraClass 311 add, (+) :: BinaryOp IsAddSemigroup 312 add = operation Addition 313 (+) = add 314 infixl 6 + 315 316 type IsMulSemigroup = IsSemigroupWith Multiplication :: AlgebraClass 317 mul, (*) :: BinaryOp IsMulSemigroup 318 mul = operation Multiplication 319 (*) = mul 320 infixl 7 * 321 322 -------------------------------------------------------------------------------- 323 324 -- | `MagmaOpK`-indexed semigroups with computable left cancellation for 325 -- left-cancellable elements 326 -- 327 -- __Laws__ (in terms of `PartiallyStrippableL`): 328 -- - /Partial left cancellation:/ if @x@ is left-cancellative, then @(x \\!) ∘ (x ⋄)@ = @identity@ 329 -- 330 -- We don't specify @(x \\!)@ on elements outside the image of @(x ⋄)@, nor do 331 -- we specify the behavior for non-left-cancellative @x@. 332 -- 333 -- Typically, monoids should also implement `PartiallyHasInverses`. 334 type PartiallyCancellableL :: MagmaClass 335 class (IsSemigroupWith op a) => PartiallyCancellableL op (a :: Type# r) where 336 pcancelL :: For op ((Partial) => Biendo a) 337 338 -- | `MagmaOpK`-indexed semigroups with computable right cancellation for 339 -- right-cancellable elements 340 -- 341 -- __Laws__ (in terms of `PartiallyStrippableR`): 342 -- - /Partial right cancellation:/ if @x@ is right-cancellative, then @(//! x) ∘ (⋄ x)@ = @identity@ 343 -- 344 -- We don't specify @(//! x)@ on elements outside the image of @(⋄ x)@, nor do 345 -- we specify the behavior for non-right-cancellative @x@. 346 -- 347 -- Typically, monoids should also implement `PartiallyHasInverses`. 348 type PartiallyCancellableR :: MagmaClass 349 class (IsSemigroupWith op a) => PartiallyCancellableR op (a :: Type# r) where 350 pcancelR :: For op ((Partial) => Biendo a) 351 352 -- | `MagmaOpK`-indexed commutative semigroups with computable cancellation for 353 -- cancellable elements 354 type PartiallyCancellable :: MagmaClass 355 class (HasCommutative op a, PartiallyCancellableL op a, PartiallyCancellableR op a) => PartiallyCancellable op (a :: Type# r) 356 357 instance (HasCommutative op a, PartiallyCancellableL op a, PartiallyCancellableR op a) => PartiallyCancellable op (a :: Type# r) 358 359 type PartiallyStrippableL = PartiallyCancellableL Combination :: AlgebraClass 360 pstripL, (\\!) :: PartialBinaryOp PartiallyStrippableL 361 pstripL = pcancelL Combination 362 (\\!) = pstripL 363 infixr 5 \\! 364 365 -- TODO: Argument order here is unintuitive. E.g., look at the Text instance. 366 type PartiallyStrippableR = PartiallyCancellableR Combination :: AlgebraClass 367 pstripR, (//!) :: PartialBinaryOp PartiallyStrippableR 368 pstripR = pcancelR Combination 369 (//!) = pstripR 370 infixl 5 //! 371 372 type PartiallyStrippable = PartiallyCancellable Combination :: AlgebraClass 373 pstrip :: PartialBinaryOp PartiallyStrippable 374 pstrip = pstripR 375 376 type PartiallySubtractableL = PartiallyCancellableL Addition :: AlgebraClass 377 psubL :: PartialBinaryOp PartiallySubtractableL 378 psubL = pcancelL Addition 379 380 type PartiallySubtractableR = PartiallyCancellableR Addition :: AlgebraClass 381 psubR :: PartialBinaryOp PartiallySubtractableR 382 psubR = pcancelR Addition 383 384 -- NOTE: There're no standard symbols for left/right-subtraction, because 385 -- usually one assumes additive operations are commutative. So we just 386 -- require commutativity for the subtraction symbols. 387 388 type PartiallySubtractable = PartiallyCancellable Addition :: AlgebraClass 389 psubtract, psub, (-!) :: PartialBinaryOp PartiallySubtractable 390 psubtract = psubL 391 psub = psubR 392 (-!) = psub 393 infixl 6 -! 394 395 type PartiallyDividableL = PartiallyCancellableL Multiplication :: AlgebraClass 396 pdivL, (\!) :: PartialBinaryOp PartiallyDividableL 397 pdivL = pcancelL Multiplication 398 (\!) = pdivL 399 infixr 7 \! 400 401 type PartiallyDividableR = PartiallyCancellableR Multiplication :: AlgebraClass 402 pdivR, (/!) :: PartialBinaryOp PartiallyDividableR 403 pdivR = pcancelR Multiplication 404 (/!) = pdivR 405 infixl 7 /! 406 407 type PartiallyDividable = PartiallyCancellable Multiplication :: AlgebraClass 408 pdiv :: PartialBinaryOp PartiallyDividable 409 pdiv = pdivR 410 411 -------------------------------------------------------------------------------- 412 413 -- | `MagmaOpK`-indexed semigroups with "decidable left cancellation" (i.e., 414 -- decidable left-cancellability and decidable images of left-operation with 415 -- left-cancellable elements) 416 -- 417 -- __Laws__ (in terms of `DecidablyStrippableL`): 418 -- - /Decidable left cancellation:/ if @x@ is left-cancellative and @y@ 419 -- factors (necessarily uniquely) as @y = x ⋄ z@, then @x \\? y@ = 420 -- @Just z@; otherwise, @x \\? y@ = @Nothing@ 421 -- 422 -- Typically, monoids should also implement `DecidablyHasInverses`. 423 type DecidablyCancellableL :: MagmaClass 424 class (PartiallyCancellableL op a) => DecidablyCancellableL op (a :: Type# r) where 425 tryCancelL# :: For op (a -> a -> Maybe# a) 426 427 tryCancelL :: forall (op :: MagmaOpK) -> BinaryOpMaybe (DecidablyCancellableL op) 428 tryCancelL op = coerce (tryCancelL# op) 429 430 -- | `MagmaOpK`-indexed semigroups with "decidable right cancellation" (i.e., 431 -- decidable right-cancellability and decidable images of right-operation with 432 -- right-cancellable elements) 433 -- 434 -- __Laws__ (in terms of `DecidablyStrippableR`): 435 -- - /Decidable right cancellation:/ if @x@ is right-cancellative and @y@ 436 -- factors (necessarily uniquely) as @y = z ⋄ x@, then @y //? x@ = 437 -- @Just z@; otherwise, @y //? x@ = @Nothing@ 438 -- 439 -- Typically, monoids should also implement `DecidablyHasInverses`. 440 type DecidablyCancellableR :: MagmaClass 441 class (PartiallyCancellableR op a) => DecidablyCancellableR op (a :: Type# r) where 442 tryCancelR# :: For op (a -> a -> Maybe# a) 443 444 tryCancelR :: forall (op :: MagmaOpK) -> BinaryOpMaybe (DecidablyCancellableR op) 445 tryCancelR op = coerce (tryCancelR# op) 446 447 -- | `MagmaOpK`-indexed commutative semigroup with "decidable cancellation" 448 -- (i.e., decidable cancellability and decidable images of operation with 449 -- cancellable elements) 450 type DecidablyCancellable :: MagmaClass 451 class (HasCommutative op a, DecidablyCancellableL op a, DecidablyCancellableR op a) => DecidablyCancellable op (a :: Type# r) 452 453 instance (HasCommutative op a, DecidablyCancellableL op a, DecidablyCancellableR op a) => DecidablyCancellable op (a :: Type# r) 454 455 type DecidablyStrippableL = DecidablyCancellableL Combination :: AlgebraClass 456 tryStripL#, (\\?#) :: BinaryOpMaybe# DecidablyStrippableL 457 tryStripL, (\\?) :: BinaryOpMaybe DecidablyStrippableL 458 tryStripL# = tryCancelL# Combination 459 (\\?#) = tryStripL# 460 tryStripL = coerce tryStripL# 461 (\\?) = tryStripL 462 infix 5 \\?#, \\? 463 464 type DecidablyStrippableR = DecidablyCancellableR Combination :: AlgebraClass 465 tryStripR#, (//?#) :: BinaryOpMaybe# DecidablyStrippableR 466 tryStripR, (//?) :: BinaryOpMaybe DecidablyStrippableR 467 tryStripR# = tryCancelR# Combination 468 (//?#) = tryStripR# 469 tryStripR = coerce tryStripR# 470 (//?) = tryStripR 471 infix 5 //?#, //? 472 473 type DecidablyStrippable = DecidablyCancellable Combination :: AlgebraClass 474 tryStrip# :: BinaryOpMaybe# DecidablyStrippable 475 tryStrip :: BinaryOpMaybe DecidablyStrippable 476 tryStrip# = tryStripR# 477 tryStrip = tryStripR 478 479 type DecidablySubtractableL = DecidablyCancellableL Addition :: AlgebraClass 480 trySubL# :: BinaryOpMaybe# DecidablySubtractableL 481 trySubL :: BinaryOpMaybe DecidablySubtractableL 482 trySubL# = tryCancelL# Addition 483 trySubL = coerce trySubL# 484 485 type DecidablySubtractableR = DecidablyCancellableR Addition :: AlgebraClass 486 trySubR# :: BinaryOpMaybe# DecidablySubtractableR 487 trySubR :: BinaryOpMaybe DecidablySubtractableR 488 trySubR# = tryCancelR# Addition 489 trySubR = coerce trySubR# 490 491 type DecidablySubtractable = DecidablyCancellable Addition :: AlgebraClass 492 trySub#, (-?#) :: BinaryOpMaybe# DecidablySubtractable 493 trySub, (-?) :: BinaryOpMaybe DecidablySubtractable 494 trySub# = trySubR# 495 (-?#) = trySub# 496 trySub = trySubR 497 (-?) = trySub 498 infix 6 -?#, -? 499 500 type DecidablyDividableL = DecidablyCancellableL Multiplication :: AlgebraClass 501 tryDivL#, (\?#) :: BinaryOpMaybe# DecidablyDividableL 502 tryDivL, (\?) :: BinaryOpMaybe DecidablyDividableL 503 tryDivL# = tryCancelL# Multiplication 504 (\?#) = tryDivL# 505 tryDivL = coerce tryDivL# 506 (\?) = tryDivL 507 infix 7 \?#, \? 508 509 type DecidablyDividableR = DecidablyCancellableR Multiplication :: AlgebraClass 510 tryDivR#, (/?#) :: BinaryOpMaybe# DecidablyDividableR 511 tryDivR, (/?) :: BinaryOpMaybe DecidablyDividableR 512 tryDivR# = tryCancelR# Multiplication 513 (/?#) = tryDivR# 514 tryDivR = coerce tryDivR# 515 (/?) = tryDivR 516 infix 7 /?#, /? 517 518 type DecidablyDividable = DecidablyCancellable Multiplication :: AlgebraClass 519 tryDiv# :: BinaryOpMaybe# DecidablyDividable 520 tryDiv :: BinaryOpMaybe DecidablyDividable 521 tryDiv# = tryDivR# 522 tryDiv = tryDivR 523 524 -------------------------------------------------------------------------------- 525 526 -- | `MagmaOpK`-indexed monoids 527 -- 528 -- __Laws__ (in terms of `IsMonoid`): 529 -- - /@nil@ is a (left and right) identity element:/ @nil ⋄ x = x = x ⋄ nil@ 530 type IsMonoidWith :: MagmaClass 531 class (IsSemigroupWith op a) => IsMonoidWith op (a :: Type# r) where 532 neutral :: For op a 533 534 type IsMonoid = IsMonoidWith Combination :: AlgebraClass 535 nil :: NullaryOp IsMonoid 536 nil = neutral Combination 537 538 type IsAddMonoid = IsMonoidWith Addition :: AlgebraClass 539 zero :: NullaryOp IsAddMonoid 540 zero = neutral Addition 541 542 type IsMulMonoid = IsMonoidWith Multiplication :: AlgebraClass 543 one :: NullaryOp IsMulMonoid 544 one = neutral Multiplication 545 546 -------------------------------------------------------------------------------- 547 548 -- NOTE: One-sided (left/right) inverses are noncanonical (and apparently not 549 -- very useful, anyway), so we only model two-sided inverses. 550 551 -- | `MagmaOpK`-indexed monoids with computable inverses for invertible elements 552 -- 553 -- __Laws__ (in terms of `PartiallyHasUndos`): 554 -- - /Partial inversion:/ if @x@ has inverse @y@, then @pundo x = y@ 555 -- 556 -- We don't specify @pundo@ on non-invertible elements. 557 type PartiallyHasInverses :: MagmaClass 558 class (IsMonoidWith op a) => PartiallyHasInverses op (a :: Type# r) where 559 pinvert :: For op ((Partial) => Endo a) 560 561 type PartiallyHasUndos = PartiallyHasInverses Combination :: AlgebraClass 562 pundo :: PartialUnaryOp PartiallyHasUndos 563 pundo = pinvert Combination 564 565 type PartiallyHasNegations = PartiallyHasInverses Addition :: AlgebraClass 566 pnegate :: PartialUnaryOp PartiallyHasNegations 567 pnegate = pinvert Addition 568 569 type PartiallyHasReciprocals = PartiallyHasInverses Multiplication :: AlgebraClass 570 precip :: PartialUnaryOp PartiallyHasReciprocals 571 precip = pinvert Multiplication 572 573 -------------------------------------------------------------------------------- 574 575 -- | `MagmaOpK`-indexed monoids with decidable invertibility and computable 576 -- inverses for invertible elements 577 -- 578 -- __Laws__ (in terms of `DecidablyHasUndos`): 579 -- - /Decidable inversion:/ if @x@ has inverse @y@, then @tryUndo x@ = 580 -- @Just y@; otherwise, @tryUndo x = Nothing@ 581 type DecidablyHasInverses :: MagmaClass 582 class (PartiallyHasInverses op a) => DecidablyHasInverses op (a :: Type# r) where 583 tryInvert# :: For op (a -> Maybe# a) 584 585 tryInvert :: forall (op :: MagmaOpK) -> UnaryOpMaybe (DecidablyHasInverses op) 586 tryInvert op = coerce (tryInvert# op) 587 588 type DecidablyHasUndos = DecidablyHasInverses Combination :: AlgebraClass 589 tryUndo# :: UnaryOpMaybe# DecidablyHasUndos 590 tryUndo :: UnaryOpMaybe DecidablyHasUndos 591 tryUndo# = tryInvert# Combination 592 tryUndo = coerce tryUndo# 593 594 type DecidablyHasNegations = DecidablyHasInverses Addition :: AlgebraClass 595 tryNegate# :: UnaryOpMaybe# DecidablyHasNegations 596 tryNegate :: UnaryOpMaybe DecidablyHasNegations 597 tryNegate# = tryInvert# Addition 598 tryNegate = coerce tryNegate# 599 600 type DecidablyHasReciprocals = DecidablyHasInverses Multiplication :: AlgebraClass 601 tryRecip# :: UnaryOpMaybe# DecidablyHasReciprocals 602 tryRecip :: UnaryOpMaybe DecidablyHasReciprocals 603 tryRecip# = tryInvert# Multiplication 604 tryRecip = coerce tryRecip# 605 606 -------------------------------------------------------------------------------- 607 608 -- | `MagmaOpK`-indexed groups 609 -- 610 -- __Laws__ (in terms of `IsGroup`): 611 -- - /Every element is invertible:/ @isJust (tryUndo x)@ = @True@ 612 type IsGroupWith :: MagmaClass 613 class (DecidablyHasInverses op a, DecidablyCancellableL op a, DecidablyCancellableR op a) => IsGroupWith op (a :: Type# r) 614 615 cancelL, cancelR :: forall (op :: MagmaOpK) -> BinaryOp (IsGroupWith op) 616 invert :: forall (op :: MagmaOpK) -> UnaryOp (IsGroupWith op) 617 cancelL op = unsafe_partial (pcancelL op) 618 cancelR op = unsafe_partial (pcancelR op) 619 invert op = unsafe_partial (pinvert op) 620 621 type IsGroup = IsGroupWith Combination :: AlgebraClass 622 stripL, (\\), stripR, (//) :: BinaryOp IsGroup 623 undo :: UnaryOp IsGroup 624 stripL = unsafe_partial pstripL 625 (\\) = unsafe_partial (\\!) 626 stripR = unsafe_partial pstripR 627 (//) = unsafe_partial (//!) 628 undo = unsafe_partial pundo 629 infixr 5 \\ 630 infixl 5 // 631 632 type IsAddGroup = IsGroupWith Addition :: AlgebraClass 633 subL, subR :: BinaryOp IsAddGroup 634 subtract, sub, (-) :: BinaryOp IsCommAddGroup 635 negate :: UnaryOp IsAddGroup 636 subL = unsafe_partial psubL 637 subR = unsafe_partial psubR 638 subtract = unsafe_partial psubtract 639 sub = unsafe_partial psub 640 (-) = unsafe_partial (-!) 641 negate = unsafe_partial pnegate 642 infixl 6 - 643 644 type IsMulGroup = IsGroupWith Multiplication :: AlgebraClass 645 divL, divR, (/) :: BinaryOp IsMulGroup -- NOTE: (\) is reserved in Haskell :( 646 div :: BinaryOp IsCommMulGroup 647 recip :: UnaryOp IsMulGroup 648 divL = unsafe_partial pdivL 649 divR = unsafe_partial pdivR 650 (/) = unsafe_partial (/!) 651 div = unsafe_partial pdiv 652 recip = unsafe_partial precip 653 infixl 7 / 654 655 -------------------------------------------------------------------------------- 656 657 -- | Commutative semigroups 658 -- 659 -- __Laws__ (in terms of `IsCommSemigroup`): 660 -- - /@combine@ is commutative:/ @x ⋄ y = y ⋄ x@ 661 type HasCommutative :: MagmaClass 662 class (IsSemigroupWith op a) => HasCommutative op (a :: Type# r) 663 664 type Commutative = HasCommutative Combination :: AlgebraClass 665 type AddCommutative = HasCommutative Addition :: AlgebraClass 666 type MulCommutative = HasCommutative Multiplication :: AlgebraClass 667 668 type IsCommSemigroup = Comm IsSemigroupWith Combination :: AlgebraClass 669 type IsCommAddSemigroup = Comm IsSemigroupWith Addition :: AlgebraClass 670 type IsCommMulSemigroup = Comm IsSemigroupWith Multiplication :: AlgebraClass 671 672 type IsCommMonoid = Comm IsMonoidWith Combination :: AlgebraClass 673 type IsCommAddMonoid = Comm IsMonoidWith Addition :: AlgebraClass 674 type IsCommMulMonoid = Comm IsMonoidWith Multiplication :: AlgebraClass 675 676 type IsCommGroup = Comm IsGroupWith Combination :: AlgebraClass 677 type IsCommAddGroup = Comm IsGroupWith Addition :: AlgebraClass 678 type IsCommMulGroup = Comm IsGroupWith Multiplication :: AlgebraClass 679 680 -------------------------------------------------------------------------------- 681 682 -- TODO: Generalize to take two MagmaK's 683 684 -- TODO: Laws 685 686 -- TODO: DecidableZero for decidable division rings (and fields)? 687 688 type IsSemiring :: AlgebraClass 689 class (IsCommAddMonoid a, IsMulMonoid a) => IsSemiring (a :: Type# r) where 690 ofNatural :: Natural -> a 691 ofNatural = \case 692 NaturalZero -> zero 693 NaturalSucc n -> app2# (+) one (ofNatural n) 694 695 type IsCommSemiring :: AlgebraClass 696 class (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r) 697 instance (IsSemiring a, MulCommutative a) => IsCommSemiring (a :: Type# r) 698 699 type IsRing :: AlgebraClass 700 class (IsSemiring a, IsAddGroup a) => IsRing (a :: Type# r) where 701 ofInteger :: Integer -> a 702 ofInteger = \case 703 IntegerNegSucc n -> negate $# ofNatural (NaturalSucc n) 704 IntegerZero -> zero 705 IntegerPosSucc n -> ofNatural (NaturalSucc n) 706 707 type IsCommRing :: AlgebraClass 708 class (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r) 709 instance (IsRing a, MulCommutative a) => IsCommRing (a :: Type# r) 710 711 type IsDivisionRing :: AlgebraClass 712 class (IsRing a, PartiallyDividableL a, PartiallyDividableR a, PartiallyHasReciprocals a) => IsDivisionRing a 713 714 type IsField :: AlgebraClass 715 class (IsDivisionRing a, MulCommutative a) => IsField a 716 instance (IsDivisionRing a, MulCommutative a) => IsField a 717 718 -- TODO: This probably doesn't belong here. 719 fromInteger :: forall {r :: Repr} (a :: Type# r). (IsSemiring a) => Integer -> a 720 fromInteger = \case 721 IntegerNegSucc _ -> panic "fromInteger on negative integer; disable NegativeLiterals" 722 IntegerZero -> ofNatural NaturalZero 723 IntegerPosSucc n -> ofNatural (NaturalSucc n) 724 {-# INLINE fromInteger #-} 725 726 -------------------------------------------------------------------------------- 727 728 baseZero :: (Base.Num a) => a 729 baseZero = 0 where fromInteger = Base.fromInteger 730 731 baseOne :: (Base.Num a) => a 732 baseOne = 1 where fromInteger = Base.fromInteger 733 734 instance (Base.Num a) => IsSemigroupWith Addition (BaseInterop a) where operation _ = coerce (Base.+) 735 instance (Base.Num a) => PartiallyCancellableL Addition (BaseInterop a) where pcancelL _ = coerce Base.subtract 736 instance (Base.Num a) => DecidablyCancellableL Addition (BaseInterop a) where tryCancelL# _ = coerce $ Just .* Base.subtract 737 instance (Base.Num a) => PartiallyCancellableR Addition (BaseInterop a) where pcancelR _ = coerce (Base.-) 738 instance (Base.Num a) => DecidablyCancellableR Addition (BaseInterop a) where tryCancelR# _ = coerce $ Just .* (Base.-) 739 instance (Base.Num a) => IsMonoidWith Addition (BaseInterop a) where neutral _ = coerce baseZero 740 instance (Base.Num a) => PartiallyHasInverses Addition (BaseInterop a) where pinvert _ = coerce Base.negate 741 instance (Base.Num a) => DecidablyHasInverses Addition (BaseInterop a) where tryInvert# _ = coerce $ Just . Base.negate 742 instance (Base.Num a) => IsGroupWith Addition (BaseInterop a) 743 instance (Base.Num a) => HasCommutative Addition (BaseInterop a) 744 instance (Base.Num a) => IsSemigroupWith Multiplication (BaseInterop a) where operation _ = coerce (Base.*) 745 instance (Base.Num a) => IsMonoidWith Multiplication (BaseInterop a) where neutral _ = coerce baseOne 746 instance (Base.Num a) => IsSemiring (BaseInterop a) where ofNatural = coerce Base.fromIntegral 747 instance (Base.Num a) => IsRing (BaseInterop a) where ofInteger = coerce Base.fromInteger 748 instance (Base.Fractional a) => PartiallyCancellableL Multiplication (BaseInterop a) where pcancelL _ = coerce \x y -> Base.recip x Base.* y 749 instance (Base.Fractional a) => PartiallyCancellableR Multiplication (BaseInterop a) where pcancelR _ = coerce (Base./) 750 instance (Base.Fractional a) => PartiallyHasInverses Multiplication (BaseInterop a) where pinvert _ = coerce Base.recip 751 instance (Base.Fractional a) => IsDivisionRing (BaseInterop a) 752 753 instance (Base.Semigroup a) => IsSemigroupWith Combination (BaseInterop a) where operation _ = coerce (Base.<>) 754 instance (Base.Monoid a) => IsMonoidWith Combination (BaseInterop a) where neutral _ = coerce Base.mempty 755 756 -------------------------------------------------------------------------------- 757 758 baseDivNonZero :: forall (a :: Type). (Base.Eq a, Base.Fractional a) => a -> a -> Maybe a 759 baseDivNonZero x y = if y Base.== baseZero then Nothing else Just (x Base./ y) 760 761 baseRecipNonZero :: forall (a :: Type). (Base.Eq a, Base.Fractional a) => a -> Maybe a 762 baseRecipNonZero x = if x Base.== baseZero then Nothing else Just (Base.recip x) 763 764 deriving via BaseInterop Natural instance IsSemigroupWith Addition Natural 765 deriving via BaseInterop Natural instance PartiallyCancellableL Addition Natural 766 instance DecidablyCancellableL Addition Natural where tryCancelL# _ = coerce $ flip Base.minusNaturalMaybe 767 deriving via BaseInterop Natural instance PartiallyCancellableR Addition Natural 768 instance DecidablyCancellableR Addition Natural where tryCancelR# _ = coerce Base.minusNaturalMaybe 769 deriving via BaseInterop Natural instance IsMonoidWith Addition Natural 770 deriving via BaseInterop Natural instance HasCommutative Addition Natural 771 deriving via BaseInterop Natural instance IsSemigroupWith Multiplication Natural 772 deriving via BaseInterop Natural instance IsMonoidWith Multiplication Natural 773 instance HasCommutative Multiplication Natural 774 deriving via BaseInterop Natural instance IsSemiring Natural 775 776 deriving via BaseInterop Integer instance IsSemigroupWith Addition Integer 777 deriving via BaseInterop Integer instance PartiallyCancellableL Addition Integer 778 deriving via BaseInterop Integer instance DecidablyCancellableL Addition Integer 779 deriving via BaseInterop Integer instance PartiallyCancellableR Addition Integer 780 deriving via BaseInterop Integer instance DecidablyCancellableR Addition Integer 781 deriving via BaseInterop Integer instance IsMonoidWith Addition Integer 782 deriving via BaseInterop Integer instance PartiallyHasInverses Addition Integer 783 deriving via BaseInterop Integer instance DecidablyHasInverses Addition Integer 784 deriving via BaseInterop Integer instance IsGroupWith Addition Integer 785 deriving via BaseInterop Integer instance HasCommutative Addition Integer 786 deriving via BaseInterop Integer instance IsSemigroupWith Multiplication Integer 787 deriving via BaseInterop Integer instance IsMonoidWith Multiplication Integer 788 instance HasCommutative Multiplication Integer 789 deriving via BaseInterop Integer instance IsSemiring Integer 790 deriving via BaseInterop Integer instance IsRing Integer 791 792 deriving via BaseInterop Rational instance IsSemigroupWith Addition Rational 793 deriving via BaseInterop Rational instance PartiallyCancellableL Addition Rational 794 deriving via BaseInterop Rational instance DecidablyCancellableL Addition Rational 795 deriving via BaseInterop Rational instance PartiallyCancellableR Addition Rational 796 deriving via BaseInterop Rational instance DecidablyCancellableR Addition Rational 797 deriving via BaseInterop Rational instance IsMonoidWith Addition Rational 798 deriving via BaseInterop Rational instance PartiallyHasInverses Addition Rational 799 deriving via BaseInterop Rational instance DecidablyHasInverses Addition Rational 800 deriving via BaseInterop Rational instance IsGroupWith Addition Rational 801 deriving via BaseInterop Rational instance HasCommutative Addition Rational 802 deriving via BaseInterop Rational instance IsSemigroupWith Multiplication Rational 803 deriving via BaseInterop Rational instance IsMonoidWith Multiplication Rational 804 instance HasCommutative Multiplication Rational 805 deriving via BaseInterop Rational instance IsSemiring Rational 806 deriving via BaseInterop Rational instance IsRing Rational 807 deriving via BaseInterop Rational instance PartiallyCancellableL Multiplication Rational 808 instance DecidablyCancellableL Multiplication Rational where tryCancelL# _ = coerce $ flip baseDivNonZero 809 deriving via BaseInterop Rational instance PartiallyCancellableR Multiplication Rational 810 instance DecidablyCancellableR Multiplication Rational where tryCancelR# _ = coerce baseDivNonZero 811 deriving via BaseInterop Rational instance PartiallyHasInverses Multiplication Rational 812 instance DecidablyHasInverses Multiplication Rational where tryInvert# _ = coerce baseRecipNonZero 813 deriving via BaseInterop Rational instance IsDivisionRing Rational 814 815 -- TODO: Switch-out base combinators for Lude's 816 instance (IsSemigroupWith op a) => IsSemigroupWith op (r -> a) where operation _ = Base.liftA2 (operation op) 817 instance (PartiallyCancellableL op a) => PartiallyCancellableL op (r -> a) where pcancelL _ = Base.liftA2 (pcancelL op) 818 instance (PartiallyCancellableR op a) => PartiallyCancellableR op (r -> a) where pcancelR _ = Base.liftA2 (pcancelR op) 819 instance (IsMonoidWith op a) => IsMonoidWith op (r -> a) where neutral _ = Base.const (neutral op) 820 instance (PartiallyHasInverses op a) => PartiallyHasInverses op (r -> a) where pinvert _ = Base.fmap (pinvert op) 821 instance (IsGroupWith op a) => DecidablyCancellableL op (r -> a) where tryCancelL# _ = just# .* cancelL op 822 instance (IsGroupWith op a) => DecidablyCancellableR op (r -> a) where tryCancelR# _ = just# .* cancelR op 823 instance (IsGroupWith op a) => DecidablyHasInverses op (r -> a) where tryInvert# _ = just# . invert op 824 instance (IsGroupWith op a) => IsGroupWith op (r -> a) 825 instance (HasCommutative op a) => HasCommutative op (r -> a) 826 instance (IsSemiring a) => IsSemiring (r -> a) where ofNatural = Base.const . ofNatural 827 instance (IsRing a) => IsRing (r -> a) where ofInteger = Base.const . ofInteger 828 829 deriving via BaseInterop Text instance IsSemigroupWith Combination Text 830 instance PartiallyCancellableL Combination Text where pcancelL _ p x = Text.stripPrefix p x ?? x 831 instance PartiallyCancellableR Combination Text where pcancelR _ x s = Text.stripSuffix s x ?? x 832 deriving via BaseInterop Text instance IsMonoidWith Combination Text 833 instance DecidablyCancellableL Combination Text where tryCancelL# _ = coerce Text.stripPrefix 834 instance DecidablyCancellableR Combination Text where tryCancelR# _ = coerce Text.stripSuffix