modular-arithmetic-1.2.1.1: A type for integers modulo some constant.

Data.Modular

Contents

Description

Types for working with integers modulo some constant.

Synopsis

# Documentation

`Mod` and its synonym `/` let you wrap arbitrary numeric types in a modulus. To work with integers (mod 7) backed by `Integer`, you could use one of the following equivalent types:

```Mod Integer 7
Integer `Mod` 7
Integer/7
ℤ/7```

(`'ℤ'` is a synonym for `Integer` provided by this library. In Emacs, you can use the TeX input mode to type it with `\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 `div` 3 :: ℤ/16
```13
`>>> ````3 * 13 :: ℤ/16
```7
```

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 `Mod` or the `/` synonym, enable `TypeOperators`:

````>>> ````:set -XTypeOperators
``````

# Modular arithmetic

data Mod i n Source

Wraps an underlying `Integeral` type `i` in a newtype annotated with the bound `n`.

Instances

 (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 `inv`, so it is possible to divide only by numbers coprime to `n` and the remainder is always `0`. (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)

unMod :: (i `Mod` n) -> i Source

Extract the underlying integral value from a modular type.

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.

````>>> ````inv 3 :: ℤ/7
```5
`>>> ````3 * 5 :: ℤ/7
```1
```

Note that only numbers coprime to `n` have an inverse modulo `n`:

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

type (/) = Mod Source

A synonym for `Mod`, inspired by the ℤ/n syntax from mathematics.

type = Integer Source

A synonym for Integer, also inspired by the ℤ/n syntax.

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

Convert an integral number `i` into a `Mod` value given modular bound `n` at type level.

data SomeMod i Source

A modular number with an unknown bound.

Instances

 Show i => Show (SomeMod i)

someModVal :: Integral i => i -> Integer -> Maybe (SomeMod i) Source

Convert an integral number `i` into a `Mod` value with an unknown modulus.