|
| 1 | +module Data.DivisionRing |
| 2 | + ( class DivisionRing |
| 3 | + , recip |
| 4 | + , leftDiv |
| 5 | + , rightDiv |
| 6 | + , module Data.Ring |
| 7 | + , module Data.Semiring |
| 8 | + ) where |
| 9 | + |
| 10 | +import Data.Ring (class Ring, negate, sub) |
| 11 | +import Data.Semiring (class Semiring, add, mul, one, zero, (*), (+)) |
| 12 | +import Data.EuclideanRing ((/)) |
| 13 | + |
| 14 | +-- | The `DivisionRing` class is for non-zero rings in which every non-zero |
| 15 | +-- | element has a multiplicative inverse. Division rings are sometimes also |
| 16 | +-- | called *skew fields*. |
| 17 | +-- | |
| 18 | +-- | Instances must satisfy the following laws in addition to the `Ring` laws: |
| 19 | +-- | |
| 20 | +-- | - Non-zero ring: `one /= zero` |
| 21 | +-- | - Non-zero multiplicative inverse: `recip a * a = a * recip a = one` for |
| 22 | +-- | all non-zero `a` |
| 23 | +-- | |
| 24 | +-- | The result of `recip zero` is left undefined; individual instances may |
| 25 | +-- | choose how to handle this case. |
| 26 | +-- | |
| 27 | +-- | If a type has both `DivisionRing` and `CommutativeRing` instances, then |
| 28 | +-- | it is a field and should have a `Field` instance. |
| 29 | +class Ring a <= DivisionRing a where |
| 30 | + recip :: a -> a |
| 31 | + |
| 32 | +-- | Left division, defined as `leftDiv a b = recip b * a`. Left and right |
| 33 | +-- | division are distinct in this module because a `DivisionRing` is not |
| 34 | +-- | necessarily commutative. |
| 35 | +-- | |
| 36 | +-- | If the type `a` is also a `EuclideanRing`, then this function is |
| 37 | +-- | equivalent to `div` from the `EuclideanRing` class. When working |
| 38 | +-- | abstractly, `div` should generally be preferred, unless you know that you |
| 39 | +-- | need your code to work with noncommutative rings. |
| 40 | +leftDiv :: forall a. DivisionRing a => a -> a -> a |
| 41 | +leftDiv a b = recip b * a |
| 42 | + |
| 43 | +-- | Right division, defined as `rightDiv a b = a * recip b`. Left and right |
| 44 | +-- | division are distinct in this module because a `DivisionRing` is not |
| 45 | +-- | necessarily commutative. |
| 46 | +-- | |
| 47 | +-- | If the type `a` is also a `EuclideanRing`, then this function is |
| 48 | +-- | equivalent to `div` from the `EuclideanRing` class. When working |
| 49 | +-- | abstractly, `div` should generally be preferred, unless you know that you |
| 50 | +-- | need your code to work with noncommutative rings. |
| 51 | +rightDiv :: forall a. DivisionRing a => a -> a -> a |
| 52 | +rightDiv a b = a * recip b |
| 53 | + |
| 54 | +instance divisionringNumber :: DivisionRing Number where |
| 55 | + recip x = 1.0 / x |
0 commit comments