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

Data.Finite

Description

Synopsis

Documentation

data Finite n Source

Finite number type. Finite n is inhabited by exactly n values. Invariants:

getFinite x < natVal x

getFinite x >= 0

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

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

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

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

finite :: KnownNat n => Integer -> Finite n Source

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

finiteProxy :: KnownNat n => proxy n -> Integer -> Finite n Source

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

getFinite :: Finite n -> Integer Source

Convert a Finite into the corresponding Integer.

equals :: Finite n -> Finite m -> Bool infix 4 Source

Test two different types of finite numbers for equality.

cmp :: Finite n -> Finite m -> Ordering Source

Compare two different types of finite numbers.

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

Convert a type-level literal into a Finite.

weaken :: Finite n -> Finite (n + 1) Source

Add one inhabitant in the end.

strengthen :: 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 :: Finite n -> Finite (n + 1) Source

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

unshift :: 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 :: n <= m => Finite n -> Finite m Source

Add multiple inhabitants in the end.

strengthenN :: (KnownNat n, n <= m) => Finite m -> Maybe (Finite n) Source

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

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

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

unshiftN :: (KnownNat n, KnownNat m, n <= m) => Finite m -> Maybe (Finite n) 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 :: proxy k -> Finite n -> Finite (n + k) Source

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

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

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

add :: Finite n -> Finite m -> Finite (n + m) Source

Add two Finites.

sub :: 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 :: Finite n -> Finite m -> Finite (n * m) Source

Multiply two Finites.

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

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

combineProduct :: 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.

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

Take a Left-biased disjoint union apart.

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

Take a fst-biased product apart.

isValidFinite :: KnownNat n => Finite n -> Bool Source

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