Data.Finite

Finite number type. The type Finite n is inhabited by exactly n values in the range [0, n) including 0 but excluding n. Invariants:

prop> getFinite x < natVal x

prop> getFinite x >= 0

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

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

Convert an Integer into a Finite, 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 into the corresponding Integer.

Generate a list of length n of all elements of Finite 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 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.