Data.Finite.Internal.Integral

Documentation

class Integral a => SaneIntegral a where

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.

Minimal complete definition

Nothing

Associated Types

type Limit a :: Maybe Nat

Methods

modAdd :: a -> a -> a -> a

Given n > 0, 0 <= a < n, and 0 <= b < n, modAdd n a b computes (a + b) ` mod ` n.

modSub :: a -> a -> a -> a

Given n > 0, 0 <= a < n, and 0 <= b < n, modSub n a b computes (a - b) ` mod ` n.

modMul :: a -> a -> a -> a

Given n > 0, 0 <= a < n, and 0 <= b < n, modMul n a b computes (a * b) ` mod ` n.

unsafeWithLimited :: proxy1 a -> proxy2 n -> (Limited a n => r) -> r

Unsafely obtain evidence that n <= Limit a. When Limit is Nothing there is no evidence to obtain, and \_ _ k -> k is a valid implementation. When Limit is a Just, the default implementation should work.

default unsafeWithLimited :: forall n r lim proxy1 proxy2. Limit a ~ 'Just lim => proxy1 a -> proxy2 n -> (Limited a n => r) -> r

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.

withLimited :: forall a n r proxy1 proxy2. (SaneIntegral a, KnownIntegral a n) => proxy1 a -> proxy2 n -> (Limited a n => r) -> r

Recover a Limited constraint from a KnownIntegral constraint.

newtype 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

Constructors

Finite a

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

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.

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

Convert a Finite a into the corresponding a.