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

Data.Finite.Internal.Integral

Description

Synopsis

# Documentation

class Integral a => SaneIntegral a where 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.

Minimal complete definition

Nothing

Associated Types

type Limit a :: Maybe Nat Source #

Methods

modAdd :: a -> a -> a -> a Source #

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

modSub :: a -> a -> a -> a Source #

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

modMul :: a -> a -> a -> a Source #

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 Source #

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 Source #

#### 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.

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

Recover a Limited constraint from a KnownIntegral constraint.

newtype 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

Constructors

 Finite a

#### Instances

Instances details
 (SaneIntegral a, KnownIntegral a n) => Bounded (Finite a n) Source # Throws an error for Finite _ 0 Instance detailsDefined in Data.Finite.Internal.Integral MethodsminBound :: Finite a n #maxBound :: Finite a n # (SaneIntegral a, KnownIntegral a n) => Enum (Finite a n) Source # Instance detailsDefined in Data.Finite.Internal.Integral Methodssucc :: 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) Source # Instance detailsDefined in Data.Finite.Internal.Integral Methodsrange :: (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) Source # +, -, and * implement arithmetic modulo n. The fromInteger function raises an error for inputs outside of bounds. Instance detailsDefined 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) Source # Instance detailsDefined in Data.Finite.Internal.Integral MethodsreadsPrec :: 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) Source # 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. Instance detailsDefined in Data.Finite.Internal.Integral Methodsquot :: 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) Source # Instance detailsDefined in Data.Finite.Internal.Integral MethodstoRational :: Finite a n -> Rational # Show a => Show (Finite a n) Source # Instance detailsDefined in Data.Finite.Internal.Integral MethodsshowsPrec :: Int -> Finite a n -> ShowS #show :: Finite a n -> String #showList :: [Finite a n] -> ShowS # NFData a => NFData (Finite a n) Source # Instance detailsDefined in Data.Finite.Internal.Integral Methodsrnf :: Finite a n -> () # Eq a => Eq (Finite a n) Source # Instance detailsDefined 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) Source # Instance detailsDefined in Data.Finite.Internal.Integral Methodscompare :: 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 Source #

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 Source #

Convert a Finite a into the corresponding a.