Numeric.Modular

The Mod m type represents a Integer modulo m, i.e., a value in ℤ/mℤ, which enables type-safe modular arithmetic.

This library, especially the withMod function, uses ideas from Functional Pearl: Implicit Configurations -- or, Type Classes Reflect the Values of Types by Oleg Kiselyov and Chung-chieh Shan, available here: http://okmij.org/ftp/Haskell/tr-15-04.pdf

For example, to perform basic modular computations,

>>> 10 :: Mod 3
1
>>> 15 + 3 :: Mod 7
4

Attempts to perform arithmetic on different modular types result in type errors.

>>> (10 :: Mod 3) + (15 :: Mod 7)
(...)error:
    • Couldn't match type ‘7’ with ‘3’
(...)

Modular reductions are performed implicitly, so modular exponentiation can be performed efficiently.

>>> 60803790666453028877 ^ 88100461154844882932 :: Mod 39127526509442054532
33479467020524411041

Compare this to running (60803790666453028877 ^ 88100461154844882932) `mod` 39127526509442054532, which is much less efficient.

The modulus can also be specified at runtime without losing any type safety or efficiency.

>>> x = mkMod 10
>>> y = mkMod 17
>>> withMod 3 (x + y)
0
>>> withMod 10 (x + y)
7
>>> a = mkMod 60803790666453028877
>>> b = 88100461154844882932 :: Integer
>>> m = 39127526509442054532 :: Integer
>>> withMod m $ a^b
33479467020524411041

Documentation

data Mod (n :: Nat)

Data type to represent an integer modulo n.

Instances

Eq (Mod m)

Defined in Numeric.Modular

Methods

(==) :: Mod m -> Mod m -> Bool

(/=) :: Mod m -> Mod m -> Bool

KnownNat m => Num (Mod m)

Defined in Numeric.Modular

Methods

(+) :: Mod m -> Mod m -> Mod m

(-) :: Mod m -> Mod m -> Mod m

(*) :: Mod m -> Mod m -> Mod m

negate :: Mod m -> Mod m

abs :: Mod m -> Mod m

signum :: Mod m -> Mod m

fromInteger :: Integer -> Mod m

KnownNat m => Show (Mod m)

Defined in Numeric.Modular

Methods

showsPrec :: Int -> Mod m -> ShowS

show :: Mod m -> String

showList :: [Mod m] -> ShowS

mkMod :: forall m. KnownNat m => Integer -> Mod m

mkMod n wraps n in type Mod m.

withMod :: Integer -> (forall m. KnownNat m => Mod m) -> Integer

In withMod m a

• m is the modulus.
• a is a value that can take on the type Mod m for any a.
• withMod m a equals a interpreted modulo m.

x = mkMod 17
withMod 5 x == 2