Safe Haskell | None |
---|---|
Language | Haskell2010 |
Types for working with integers modulo some constant.
Synopsis
- data Mod i (n :: Nat)
- type Modulus n = (KnownNat n, 1 <= n)
- unMod :: (i `Mod` n) -> i
- toMod :: forall n i. (Integral i, Modulus n) => i -> i `Mod` n
- toMod' :: forall n i j. (Integral i, Integral j, Modulus n) => i -> j `Mod` n
- inv :: forall n i. (Modulus n, Integral i) => (i / n) -> Maybe (i / n)
- type (/) = Mod
- type ℤ = Integer
- modVal :: forall i proxy n. (Integral i, Modulus n) => i -> proxy n -> Mod i n
- data SomeMod i
- someModVal :: Integral i => i -> Integer -> Maybe (SomeMod i)
Documentation
and its synonym Mod
/
let you wrap arbitrary numeric types
in a modulus. To work with integers (mod 7) backed by
,
you could use one of the following equivalent types:Integer
Mod Integer 7 Integer `Mod` 7 Integer/7 ℤ/7
(
is a synonym for ℤ
provided by this library. In
Emacs, you can use the TeX input mode to type it with Integer
\Bbb{Z}
.)
The usual numeric typeclasses are defined for these types. You can
always extract the underlying value with
.unMod
Here is a quick example:
>>>
10 * 11 :: ℤ/7
5
It also works correctly with negative numeric literals:
>>>
(-10) * 11 :: ℤ/7
2
Modular division is an inverse of modular multiplication. It is defined when divisor is coprime to modulus:
>>>
7 / 3 :: ℤ/16
13>>>
3 * 13 :: ℤ/16
7
Note that it raises an exception if the divisor is *not* coprime to the modulus:
>>>
7 / 4 :: ℤ/16
*** Exception: Cannot invert 4 (mod 16): not coprime to modulus. ...
To use type level numeric literals you need to enable the
DataKinds
extension and to use infix syntax for Mod
or the /
synonym, you need TypeOperators
.
Preliminaries
To use type level numeric literals you need to enable
the DataKinds
extension:
>>>
:set -XDataKinds
To use infix syntax for
or the Mod
/
synonym,
enable TypeOperators
:
>>>
:set -XTypeOperators
To use type applications with
and friends:toMod
>>>
:set -XTypeApplications
Modular arithmetic
data Mod i (n :: Nat) Source #
Wraps an underlying Integeral
type i
in a newtype annotated
with the bound n
.
Instances
(Integral i, Modulus n) => Bounded (Mod i n) Source # | |
(Integral i, Modulus n) => Enum (Mod i n) Source # | |
Eq i => Eq (Mod i n) Source # | |
(Integral i, Modulus n) => Fractional (Mod i n) Source # | Division uses modular inverse
Dividing by a number that is not coprime to
|
(Integral i, Modulus n) => Num (Mod i n) Source # | |
Ord i => Ord (Mod i n) Source # | |
(Read i, Integral i, Modulus n) => Read (Mod i n) Source # | |
(Integral i, Modulus n) => Real (Mod i n) Source # | |
Defined in Data.Modular toRational :: Mod i n -> Rational # | |
Show i => Show (Mod i n) Source # | |
type Modulus n = (KnownNat n, 1 <= n) Source #
The modulus has to be a non-zero type-level natural number.
unMod :: (i `Mod` n) -> i Source #
Extract the underlying integral value from a modular type.
>>>
unMod (10 :: ℤ/4)
2
toMod :: forall n i. (Integral i, Modulus n) => i -> i `Mod` n Source #
Injects a value of the underlying type into the modulus type, wrapping as appropriate.
If n
is ambiguous, you can specify it with TypeApplications
:
>>>
toMod @6 10
4
Note that n
cannot be 0.
toMod' :: forall n i j. (Integral i, Integral j, Modulus n) => i -> j `Mod` n Source #
Wraps an integral number, converting between integral types.
inv :: forall n i. (Modulus n, Integral i) => (i / n) -> Maybe (i / n) Source #
The modular inverse.
>>>
inv 3 :: Maybe (ℤ/7)
Just 5>>>
3 * 5 :: ℤ/7
1
Note that only numbers coprime to n
have an inverse modulo n
:
>>>
inv 6 :: Maybe (ℤ/15)
Nothing
A modular number with an unknown modulus.
Conceptually SomeMod i = ∃n. i/n
.
Instances
Show i => Show (SomeMod i) Source # | Shows both the number *and* its modulus:
This doesn't *quite* follow the rule that the show instance should
be a Haskell expression that evaluates to the given
value— |
Convert an integral number i
into
with the modulus
given at runtime.SomeMod
That is, given i :: ℤ
, someModVal i modulus
is equivalent to i ::
ℤ/modulus
except we don't know modulus
statically.
>>>
someModVal 10 4
Just (someModVal 2 4)
Will return Nothing
if the modulus is 0 or negative:
>>>
someModVal 10 (-10)
Nothing
>>>
someModVal 10 0
Nothing