Safe Haskell | None |
---|---|

Language | Haskell98 |

Types for working with integers modulo some constant.

- data Mod i n
- unMod :: (i `Mod` n) -> i
- toMod :: forall n i. (Integral i, KnownNat n) => i -> i `Mod` n
- toMod' :: forall n i j. (Integral i, Integral j, KnownNat n) => i -> j `Mod` n
- inv :: forall n i. (KnownNat n, Integral i) => Mod i n -> Mod i n
- type (/) = Mod
- type ℤ = Integer
- modVal :: forall i proxy n. (Integral i, KnownNat 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:

`>>>`

5`10 * 11 :: ℤ/7`

It also works correctly with negative numeric literals:

`>>>`

2`(-10) * 11 :: ℤ/7`

Modular division is an inverse of modular multiplication. It is defined when divisor is coprime to modulus:

`>>>`

13`7 `div` 3 :: ℤ/16`

`>>>`

7`3 * 13 :: ℤ/16`

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`

# Modular arithmetic

Wraps an underlying `Integeral`

type `i`

in a newtype annotated
with the bound `n`

.

(Integral i, KnownNat n) => Bounded (Mod i n) | |

(Integral i, KnownNat n) => Enum (Mod i n) | |

Eq i => Eq (Mod i n) | |

(Integral i, KnownNat n) => Integral (Mod i n) | Integer division uses modular inverse |

(Integral i, KnownNat n) => Num (Mod i n) | |

Ord i => Ord (Mod i n) | |

(Read i, Integral i, KnownNat n) => Read (Mod i n) | |

(Integral i, KnownNat n) => Real (Mod i n) | |

Show i => Show (Mod i n) |

toMod :: forall n i. (Integral i, KnownNat n) => i -> i `Mod` n Source

Injects a value of the underlying type into the modulus type, wrapping as appropriate.

toMod' :: forall n i j. (Integral i, Integral j, KnownNat n) => i -> j `Mod` n Source

Wraps an integral number, converting between integral types.

inv :: forall n i. (KnownNat n, Integral i) => Mod i n -> Mod i n Source

The modular inverse.

`>>>`

5`inv 3 :: ℤ/7`

`>>>`

1`3 * 5 :: ℤ/7`

Note that only numbers coprime to `n`

have an inverse modulo `n`

:

`>>>`

*** Exception: divide by 6 (mod 15), non-coprime to modulus`inv 6 :: ℤ/15`