Copyright	(C) 2015-2022 mniip
License	BSD3
Maintainer	mniip <mniip@mniip.com>
Stability	experimental
Portability	portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Finite

Description

Synopsis

type Finite = Finite Integer
packFinite :: forall n. KnownNat n => Integer -> Maybe (Finite n)
packFiniteProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Maybe (Finite n)
finite :: forall n. KnownNat n => Integer -> Finite n
finiteProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n
getFinite :: forall n. Finite n -> Integer
finites :: forall n. KnownNat n => [Finite n]
finitesProxy :: forall n proxy. KnownNat n => proxy n -> [Finite n]
modulo :: forall n. KnownNat n => Integer -> Finite n
moduloProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n
equals :: forall n m. Finite n -> Finite m -> Bool
cmp :: forall n m. Finite n -> Finite m -> Ordering
natToFinite :: forall n m proxy. (KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m
weaken :: forall n. Finite n -> Finite (n + 1)
strengthen :: forall n. KnownNat n => Finite (n + 1) -> Maybe (Finite n)
shift :: forall n. Finite n -> Finite (n + 1)
unshift :: forall n. Finite (n + 1) -> Maybe (Finite n)
weakenN :: forall n m. n <= m => Finite n -> Finite m
strengthenN :: forall n m. KnownNat m => Finite n -> Maybe (Finite m)
shiftN :: forall n m. (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m
unshiftN :: forall n m. (KnownNat n, KnownNat m) => Finite n -> Maybe (Finite m)
weakenProxy :: forall n k proxy. proxy k -> Finite n -> Finite (n + k)
strengthenProxy :: forall n k proxy. KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n)
shiftProxy :: forall n k proxy. KnownNat k => proxy k -> Finite n -> Finite (n + k)
unshiftProxy :: forall n k proxy. KnownNat k => proxy k -> Finite (n + k) -> Maybe (Finite n)
add :: forall n m. Finite n -> Finite m -> Finite (n + m)
sub :: forall n m. Finite n -> Finite m -> Either (Finite m) (Finite n)
multiply :: forall n m. Finite n -> Finite m -> Finite (n * m)
combineSum :: forall n m. KnownNat n => Either (Finite n) (Finite m) -> Finite (n + m)
combineZero :: Void -> Finite 0
combineProduct :: forall n m. KnownNat n => (Finite n, Finite m) -> Finite (n * m)
combineOne :: () -> Finite 1
combineExponential :: forall n m. (KnownNat m, KnownNat n) => (Finite n -> Finite m) -> Finite (m ^ n)
separateSum :: forall n m. KnownNat n => Finite (n + m) -> Either (Finite n) (Finite m)
separateZero :: Finite 0 -> Void
separateProduct :: forall n m. KnownNat n => Finite (n * m) -> (Finite n, Finite m)
separateOne :: Finite 1 -> ()
separateExponential :: forall n m. KnownNat m => Finite (m ^ n) -> Finite n -> Finite m
isValidFinite :: forall n. KnownNat n => Finite n -> Bool

Documentation

type Finite = Finite Integer Source #

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

getFinite x < natVal x

getFinite x >= 0

packFinite :: forall n. KnownNat n => Integer -> Maybe (Finite n) Source #

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

packFiniteProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Maybe (Finite n) Source #

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

finite :: forall n. KnownNat n => Integer -> Finite n Source #

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

finiteProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n Source #

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

getFinite :: forall n. Finite n -> Integer Source #

Convert a Finite into the corresponding Integer.

finites :: forall n. KnownNat n => [Finite n] Source #

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

finitesProxy :: forall n proxy. KnownNat n => proxy n -> [Finite n] Source #

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

modulo :: forall n. KnownNat n => Integer -> Finite n Source #

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

moduloProxy :: forall n proxy. KnownNat n => proxy n -> Integer -> Finite n Source #

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

equals :: forall n m. Finite n -> Finite m -> Bool infix 4 Source #

Test two different types of finite numbers for equality.

cmp :: forall n m. Finite n -> Finite m -> Ordering Source #

Compare two different types of finite numbers.

natToFinite :: forall n m proxy. (KnownNat n, KnownNat m, (n + 1) <= m) => proxy n -> Finite m Source #

Convert a type-level literal into a Finite.

weaken :: forall n. Finite n -> Finite (n + 1) Source #

Add one inhabitant in the end.

strengthen :: forall n. KnownNat n => Finite (n + 1) -> Maybe (Finite n) Source #

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

shift :: forall n. Finite n -> Finite (n + 1) Source #

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

unshift :: forall n. Finite (n + 1) -> Maybe (Finite n) Source #

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

weakenN :: forall n m. n <= m => Finite n -> Finite m Source #

Add multiple inhabitants in the end.

strengthenN :: forall n m. KnownNat m => Finite n -> Maybe (Finite m) Source #

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

shiftN :: forall n m. (KnownNat n, KnownNat m, n <= m) => Finite n -> Finite m Source #

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

unshiftN :: forall n m. (KnownNat n, KnownNat m) => Finite n -> Maybe (Finite m) Source #

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.

weakenProxy :: forall n k proxy. proxy k -> Finite n -> Finite (n + k) Source #

strengthenProxy :: forall n k proxy. KnownNat n => proxy k -> Finite (n + k) -> Maybe (Finite n) Source #

shiftProxy :: forall n k proxy. KnownNat k => proxy k -> Finite n -> Finite (n + k) Source #

unshiftProxy :: forall n k proxy. KnownNat k => proxy k -> Finite (n + k) -> Maybe (Finite n) Source #

add :: forall n m. Finite n -> Finite m -> Finite (n + m) Source #

Add two Finites.

sub :: forall n m. Finite n -> Finite m -> Either (Finite m) (Finite n) Source #

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

multiply :: forall n m. Finite n -> Finite m -> Finite (n * m) Source #

Multiply two Finites.

combineSum :: forall n m. KnownNat n => Either (Finite n) (Finite m) -> Finite (n + m) Source #

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

combineZero :: Void -> Finite 0 Source #

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

combineProduct :: forall n m. KnownNat n => (Finite n, Finite m) -> Finite (n * m) Source #

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

combineOne :: () -> Finite 1 Source #

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

combineExponential :: forall n m. (KnownNat m, KnownNat n) => (Finite n -> Finite m) -> Finite (m ^ n) Source #

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

separateSum :: forall n m. KnownNat n => Finite (n + m) -> Either (Finite n) (Finite m) Source #

Take a Left-biased disjoint union apart.

separateZero :: Finite 0 -> Void Source #

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.

separateProduct :: forall n m. KnownNat n => Finite (n * m) -> (Finite n, Finite m) Source #

Take a fst-biased product apart.

separateOne :: Finite 1 -> () Source #

separateExponential :: forall n m. KnownNat m => Finite (m ^ n) -> Finite n -> Finite m Source #

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

isValidFinite :: forall n. KnownNat n => Finite n -> Bool Source #

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.