Data.Finite.Integral

A class of datatypes that faithfully represent a sub-range of Integer that includes 0. A valid instance must obey the following laws:

fromInteger must be a retract of toInteger:

prop> fromInteger (toInteger a) == a

Restricted to the range [0, Limit] (with Nothing understood as positive infinity), fromInteger must be an inverse of toInteger:

prop> limited i ==> toInteger (fromInteger i) == i

where:

limited i = case limit of
    Just l -> 0 <= i && i <= l
    Nothing -> 0 <= i

WARNING: violating the above constraint in particular breaks type safety.

The implementations of Ord, Enum, Num, Integral must be compatible with that of Integer, whenever all arguments and results fall within [0, Limit], for example:

prop> limited i && limited j && limited k && (i * j == k) ==> (fromInteger i * fromInteger j == fromInteger k)

Methods modAdd, modSub, and modMul implement modular addition, multiplication, and subtraction. The default implementation is via Integer, but a faster implementation can be provided instead. If provided, the implementation must be correct for moduli in range [1, Limit].

WARNING: a naive implementaton is prone to arithmetic overflow and may produce invalid results for moduli close to Limit.

Ensures that the value of n is representable in type a (which should be a SaneIntegral).

This class asserts that the value of n is known at runtime, and that it is representable in type a (which should be a SaneIntegral).

At runtime it acts like an implicit parameter of type a, much like KnownNat is an implicit parameter of type Integer.

Reflect a type-level number into a term.

Recover a KnownNat constraint from a KnownIntegral constraint.

Finite number type. The type Finite a n is inhabited by exactly n values from type a, in the range [0, n) including 0 but excluding n. a must be an instance of SaneIntegral to use this type. Invariants:

prop> getFinite x < intVal x

prop> getFinite x >= 0

Convert an a into a Finite a, returning Nothing if the input is out of bounds.

Same as packFinite but with a proxy argument to avoid type signatures.

Convert an a into a Finite a, throwing an error if the input is out of bounds.

Same as finite but with a proxy argument to avoid type signatures.

Convert a Finite a into the corresponding a.

Generate an ascending list of length n of all elements of Finite a n.

Same as finites but with a proxy argument to avoid type signatures.

Produce the Finite that is congruent to the given integer modulo n.

Same as modulo but with a proxy argument to avoid type signatures.

Test two different types of finite numbers for equality.

Compare two different types of finite numbers.

Convert a type-level literal into a Finite.

Add one inhabitant in the end.

Remove one inhabitant from the end. Returns Nothing if the input was the removed inhabitant.

Add one inhabitant in the beginning, shifting everything up by one.

Remove one inhabitant from the beginning, shifting everything down by one. Returns Nothing if the input was the removed inhabitant.

Add multiple inhabitants in the end.

Remove multiple inhabitants from the end. Returns Nothing if the input was one of the removed inhabitants.

Add multiple inhabitants in the beginning, shifting everything up by the amount of inhabitants added.

Remove multiple inhabitants from the beginning, shifting everything down by the amount of inhabitants removed. Returns Nothing if the input was one of the removed inhabitants.

Add two Finites.

Subtract two Finites. Returns Left for negative results, and Right for positive results. Note that this function never returns Left 0.

Multiply two Finites.

Left-biased (left values come first) disjoint union of finite sets.

Witness that combineSum preserves units: 0 is the unit of +, and Void is the unit of Either.

fst-biased (fst is the inner, and snd is the outer iteratee) product of finite sets.

Witness that combineProduct preserves units: 1 is the unit of *, and () is the unit of (,).

Product of n copies of a finite set of size m, biased towards the lower values of the argument (colex order).

Take a Left-biased disjoint union apart.

Witness that separateSum preserves units: 0 is the unit of +, and Void is the unit of Either.

Also witness that a Finite a 0 is uninhabited.

Take a fst-biased product apart.

Take a product of n copies of a finite set of size m apart, biased towards the lower values of the argument (colex order).

Verifies that a given Finite is valid. Should always return True unless you bring the Data.Finite.Internal.Finite constructor into the scope, or use unsafeCoerce or other nasty hacks.