finite-typelits-0.2.1.0: A type inhabited by finitely many values, indexed by type-level naturals

Data.Finite.Integral

Description

Synopsis

# Documentation

class Integral a => SaneIntegral a Source #

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:

fromInteger (toInteger a) == a

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

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:

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.

#### Instances

Instances details
 Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int16 -> proxy2 n -> (Limited Int16 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int32 -> proxy2 n -> (Limited Int32 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int64 -> proxy2 n -> (Limited Int64 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Typestype Limit Int8 :: Maybe Nat Source # MethodsmodAdd :: Int8 -> Int8 -> Int8 -> Int8 Source #modSub :: Int8 -> Int8 -> Int8 -> Int8 Source #modMul :: Int8 -> Int8 -> Int8 -> Int8 Source #unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int8 -> proxy2 n -> (Limited Int8 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word16 -> proxy2 n -> (Limited Word16 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word32 -> proxy2 n -> (Limited Word32 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word64 -> proxy2 n -> (Limited Word64 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word8 -> proxy2 n -> (Limited Word8 n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Integer -> proxy2 n -> (Limited Integer n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Types MethodsunsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Natural -> proxy2 n -> (Limited Natural n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Typestype Limit Int :: Maybe Nat Source # MethodsmodAdd :: Int -> Int -> Int -> Int Source #modSub :: Int -> Int -> Int -> Int Source #modMul :: Int -> Int -> Int -> Int Source #unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int -> proxy2 n -> (Limited Int n => r) -> r Source # Source # Instance detailsDefined in Data.Finite.Internal.Integral Associated Typestype Limit Word :: Maybe Nat Source # MethodsmodAdd :: Word -> Word -> Word -> Word Source #modSub :: Word -> Word -> Word -> Word Source #modMul :: Word -> Word -> Word -> Word Source #unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word -> proxy2 n -> (Limited Word n => r) -> r Source #

type Limited a (n :: Nat) = LeqMaybe n (Limit a) Source #

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

class KnownIntegral a (n :: Nat) Source #

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.

Minimal complete definition

intVal_

#### Instances

Instances details
 (SaneIntegral a, Limited a n, KnownNat n) => KnownIntegral a n Source # Instance detailsDefined in Data.Finite.Internal.Integral MethodsintVal_ :: Tagged n a

intVal :: forall n a proxy. KnownIntegral a n => proxy n -> a Source #

Reflect a type-level number into a term.

withIntegral :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n) => proxy1 a -> proxy2 n -> (KnownNat n => r) -> r Source #

Recover a KnownNat constraint from a KnownIntegral constraint.

data Finite a (n :: Nat) Source #

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:

getFinite x < intVal x
getFinite x >= 0

#### Instances

Instances details

packFinite :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Maybe (Finite a n) Source #

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

packFiniteProxy :: forall n a proxy. (SaneIntegral a, KnownIntegral a n) => proxy n -> a -> Maybe (Finite a n) Source #

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

finite :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Finite a n Source #

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

finiteProxy :: forall n a proxy. (SaneIntegral a, KnownIntegral a n) => proxy n -> a -> Finite a n Source #

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

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

Convert a Finite a into the corresponding a.

finites :: forall n a. (SaneIntegral a, KnownIntegral a n) => [Finite a n] Source #

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

finitesProxy :: forall n a proxy. (SaneIntegral a, KnownIntegral a n) => proxy n -> [Finite a n] Source #

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

modulo :: forall n a. (SaneIntegral a, KnownIntegral a n) => a -> Finite a n Source #

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

moduloProxy :: forall n a proxy. (SaneIntegral a, KnownIntegral a n) => proxy n -> a -> Finite a n Source #

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

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

Test two different types of finite numbers for equality.

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

Compare two different types of finite numbers.

natToFinite :: forall n m a proxy. (SaneIntegral a, KnownIntegral a n, Limited a m, (n + 1) <= m) => proxy n -> Finite a m Source #

Convert a type-level literal into a Finite.

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

Add one inhabitant in the end.

strengthen :: forall n a. (SaneIntegral a, KnownIntegral a n) => Finite a (n + 1) -> Maybe (Finite a n) Source #

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

shift :: forall n a. (SaneIntegral a, Limited a (n + 1)) => Finite a n -> Finite a (n + 1) Source #

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

unshift :: forall n a. SaneIntegral a => Finite a (n + 1) -> Maybe (Finite a 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 a. (n <= m, Limited a m) => Finite a n -> Finite a m Source #

Add multiple inhabitants in the end.

strengthenN :: forall n m a. (SaneIntegral a, KnownIntegral a m, Limited a m) => Finite a n -> Maybe (Finite a m) Source #

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

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

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

unshiftN :: forall n m a. (SaneIntegral a, KnownIntegral a n, KnownIntegral a m, Limited a m) => Finite a n -> Maybe (Finite a 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 a proxy. Limited a (n + k) => proxy k -> Finite a n -> Finite a (n + k) Source #

strengthenProxy :: forall n k a proxy. (SaneIntegral a, KnownIntegral a n) => proxy k -> Finite a (n + k) -> Maybe (Finite a n) Source #

shiftProxy :: forall n k a proxy. (SaneIntegral a, KnownIntegral a k, Limited a (n + k)) => proxy k -> Finite a n -> Finite a (n + k) Source #

unshiftProxy :: forall n k a proxy. (SaneIntegral a, KnownIntegral a k) => proxy k -> Finite a (n + k) -> Maybe (Finite a n) Source #

add :: forall n m a. (SaneIntegral a, Limited a (n + m)) => Finite a n -> Finite a m -> Finite a (n + m) Source #

sub :: forall n m a. SaneIntegral a => Finite a n -> Finite a m -> Either (Finite a m) (Finite a 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 a. (SaneIntegral a, Limited a (n * m)) => Finite a n -> Finite a m -> Finite a (n * m) Source #

Multiply two Finites.

combineSum :: forall n m a. (SaneIntegral a, KnownIntegral a n, Limited a (n + m)) => Either (Finite a n) (Finite a m) -> Finite a (n + m) Source #

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

combineZero :: forall a. Void -> Finite a 0 Source #

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

combineProduct :: forall n m a. (SaneIntegral a, KnownIntegral a n, Limited a (n * m)) => (Finite a n, Finite a m) -> Finite a (n * m) Source #

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

combineOne :: forall a. (SaneIntegral a, Limited a 1) => () -> Finite a 1 Source #

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

combineExponential :: forall n m a. (SaneIntegral a, KnownIntegral a m, KnownIntegral a n, Limited a (m ^ n)) => (Finite a n -> Finite a m) -> Finite a (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 a. (SaneIntegral a, KnownIntegral a n) => Finite a (n + m) -> Either (Finite a n) (Finite a m) Source #

Take a Left-biased disjoint union apart.

separateZero :: forall a. SaneIntegral a => Finite a 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 a 0 is uninhabited.

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

Take a fst-biased product apart.

separateOne :: forall a. Finite a 1 -> () Source #

separateExponential :: forall n m a. (SaneIntegral a, KnownIntegral a m) => Finite a (m ^ n) -> Finite a n -> Finite a 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).

castFinite :: forall b a n. (SaneIntegral a, SaneIntegral b, Limited b n) => Finite a n -> Finite b n Source #

Convert a Finite between different SaneIntegral numeric types.

isValidFinite :: forall n a. (Ord a, Num a, KnownIntegral a n) => Finite a 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.