Data.Finite.Integral

Documentation

class Integral a => SaneIntegral a

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

SaneIntegral Int16

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Int16 :: Maybe Nat

Methods

modAdd :: Int16 -> Int16 -> Int16 -> Int16

modSub :: Int16 -> Int16 -> Int16 -> Int16

modMul :: Int16 -> Int16 -> Int16 -> Int16

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int16 -> proxy2 n -> (Limited Int16 n => r) -> r

SaneIntegral Int32

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Int32 :: Maybe Nat

Methods

modAdd :: Int32 -> Int32 -> Int32 -> Int32

modSub :: Int32 -> Int32 -> Int32 -> Int32

modMul :: Int32 -> Int32 -> Int32 -> Int32

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int32 -> proxy2 n -> (Limited Int32 n => r) -> r

SaneIntegral Int64

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Int64 :: Maybe Nat

Methods

modAdd :: Int64 -> Int64 -> Int64 -> Int64

modSub :: Int64 -> Int64 -> Int64 -> Int64

modMul :: Int64 -> Int64 -> Int64 -> Int64

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int64 -> proxy2 n -> (Limited Int64 n => r) -> r

SaneIntegral Int8

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Int8 :: Maybe Nat

Methods

modAdd :: Int8 -> Int8 -> Int8 -> Int8

modSub :: Int8 -> Int8 -> Int8 -> Int8

modMul :: Int8 -> Int8 -> Int8 -> Int8

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int8 -> proxy2 n -> (Limited Int8 n => r) -> r

SaneIntegral Word16

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Word16 :: Maybe Nat

Methods

modAdd :: Word16 -> Word16 -> Word16 -> Word16

modSub :: Word16 -> Word16 -> Word16 -> Word16

modMul :: Word16 -> Word16 -> Word16 -> Word16

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word16 -> proxy2 n -> (Limited Word16 n => r) -> r

SaneIntegral Word32

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Word32 :: Maybe Nat

Methods

modAdd :: Word32 -> Word32 -> Word32 -> Word32

modSub :: Word32 -> Word32 -> Word32 -> Word32

modMul :: Word32 -> Word32 -> Word32 -> Word32

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word32 -> proxy2 n -> (Limited Word32 n => r) -> r

SaneIntegral Word64

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Word64 :: Maybe Nat

Methods

modAdd :: Word64 -> Word64 -> Word64 -> Word64

modSub :: Word64 -> Word64 -> Word64 -> Word64

modMul :: Word64 -> Word64 -> Word64 -> Word64

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word64 -> proxy2 n -> (Limited Word64 n => r) -> r

SaneIntegral Word8

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Word8 :: Maybe Nat

Methods

modAdd :: Word8 -> Word8 -> Word8 -> Word8

modSub :: Word8 -> Word8 -> Word8 -> Word8

modMul :: Word8 -> Word8 -> Word8 -> Word8

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word8 -> proxy2 n -> (Limited Word8 n => r) -> r

SaneIntegral Integer

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Integer :: Maybe Nat

Methods

modAdd :: Integer -> Integer -> Integer -> Integer

modSub :: Integer -> Integer -> Integer -> Integer

modMul :: Integer -> Integer -> Integer -> Integer

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Integer -> proxy2 n -> (Limited Integer n => r) -> r

SaneIntegral Natural

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Natural :: Maybe Nat

Methods

modAdd :: Natural -> Natural -> Natural -> Natural

modSub :: Natural -> Natural -> Natural -> Natural

modMul :: Natural -> Natural -> Natural -> Natural

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Natural -> proxy2 n -> (Limited Natural n => r) -> r

SaneIntegral Int

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Int :: Maybe Nat

Methods

modAdd :: Int -> Int -> Int -> Int

modSub :: Int -> Int -> Int -> Int

modMul :: Int -> Int -> Int -> Int

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Int -> proxy2 n -> (Limited Int n => r) -> r

SaneIntegral Word

Defined in Data.Finite.Internal.Integral

Associated Types

type Limit Word :: Maybe Nat

Methods

modAdd :: Word -> Word -> Word -> Word

modSub :: Word -> Word -> Word -> Word

modMul :: Word -> Word -> Word -> Word

unsafeWithLimited :: forall proxy1 proxy2 (n :: Nat) r. proxy1 Word -> proxy2 n -> (Limited Word n => r) -> r

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

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

class KnownIntegral a (n :: Nat)

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

(SaneIntegral a, Limited a n, KnownNat n) => KnownIntegral a n

Defined in Data.Finite.Internal.Integral

Methods

intVal_ :: Tagged n a

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

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

Recover a KnownNat constraint from a KnownIntegral constraint.

data Finite a (n :: Nat)

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

(SaneIntegral a, KnownIntegral a n) => Bounded (Finite a n)

Throws an error for Finite _ 0

Defined in Data.Finite.Internal.Integral

Methods

minBound :: Finite a n

maxBound :: Finite a n

(SaneIntegral a, KnownIntegral a n) => Enum (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

succ :: Finite a n -> Finite a n

pred :: Finite a n -> Finite a n

toEnum :: Int -> Finite a n

fromEnum :: Finite a n -> Int

enumFrom :: Finite a n -> [Finite a n]

enumFromThen :: Finite a n -> Finite a n -> [Finite a n]

enumFromTo :: Finite a n -> Finite a n -> [Finite a n]

enumFromThenTo :: Finite a n -> Finite a n -> Finite a n -> [Finite a n]

Ix a => Ix (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

range :: (Finite a n, Finite a n) -> [Finite a n]

index :: (Finite a n, Finite a n) -> Finite a n -> Int

unsafeIndex :: (Finite a n, Finite a n) -> Finite a n -> Int

inRange :: (Finite a n, Finite a n) -> Finite a n -> Bool

rangeSize :: (Finite a n, Finite a n) -> Int

unsafeRangeSize :: (Finite a n, Finite a n) -> Int

(SaneIntegral a, KnownIntegral a n) => Num (Finite a n)

+, -, and * implement arithmetic modulo n. The fromInteger function raises an error for inputs outside of bounds.

Defined in Data.Finite.Internal.Integral

Methods

(+) :: Finite a n -> Finite a n -> Finite a n

(-) :: Finite a n -> Finite a n -> Finite a n

(*) :: Finite a n -> Finite a n -> Finite a n

negate :: Finite a n -> Finite a n

abs :: Finite a n -> Finite a n

signum :: Finite a n -> Finite a n

fromInteger :: Integer -> Finite a n

(Read a, SaneIntegral a, KnownIntegral a n) => Read (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

readsPrec :: Int -> ReadS (Finite a n)

readList :: ReadS [Finite a n]

readPrec :: ReadPrec (Finite a n)

readListPrec :: ReadPrec [Finite a n]

(SaneIntegral a, KnownIntegral a n) => Integral (Finite a n)

quot and rem are the same as div and mod and they implement regular division of numbers in the range [0, n), not modular inverses.

Defined in Data.Finite.Internal.Integral

Methods

quot :: Finite a n -> Finite a n -> Finite a n

rem :: Finite a n -> Finite a n -> Finite a n

div :: Finite a n -> Finite a n -> Finite a n

mod :: Finite a n -> Finite a n -> Finite a n

quotRem :: Finite a n -> Finite a n -> (Finite a n, Finite a n)

divMod :: Finite a n -> Finite a n -> (Finite a n, Finite a n)

toInteger :: Finite a n -> Integer

(SaneIntegral a, KnownIntegral a n) => Real (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

toRational :: Finite a n -> Rational

Show a => Show (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

showsPrec :: Int -> Finite a n -> ShowS

show :: Finite a n -> String

showList :: [Finite a n] -> ShowS

NFData a => NFData (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

rnf :: Finite a n -> ()

Eq a => Eq (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

(==) :: Finite a n -> Finite a n -> Bool

(/=) :: Finite a n -> Finite a n -> Bool

Ord a => Ord (Finite a n)

Defined in Data.Finite.Internal.Integral

Methods

compare :: Finite a n -> Finite a n -> Ordering

(<) :: Finite a n -> Finite a n -> Bool

(<=) :: Finite a n -> Finite a n -> Bool

(>) :: Finite a n -> Finite a n -> Bool

(>=) :: Finite a n -> Finite a n -> Bool

max :: Finite a n -> Finite a n -> Finite a n

min :: Finite a n -> Finite a n -> Finite a n

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

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)

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

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

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

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

Convert a Finite a into the corresponding a.

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

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]

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

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

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

Test two different types of finite numbers for equality.

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

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

Convert a type-level literal into a Finite.

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

Add one inhabitant in the end.

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

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)

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)

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

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)

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

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)

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)

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

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

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

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

Add two Finites.

sub :: forall n m a. SaneIntegral a => Finite a n -> Finite a m -> Either (Finite a m) (Finite a n)

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)

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)

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

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

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)

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

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)

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)

Take a Left-biased disjoint union apart.

separateZero :: forall a. SaneIntegral a => Finite a 0 -> Void

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)

Take a fst-biased product apart.

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

separateExponential :: forall n m a. (SaneIntegral a, KnownIntegral a m) => Finite a (m ^ n) -> Finite a n -> Finite a m

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

Convert a Finite between different SaneIntegral numeric types.

isValidFinite :: forall n a. (Ord a, Num a, KnownIntegral a n) => Finite a n -> Bool

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.