Data.Fin.Int.Explicit

Finite natural numbers, with upper bound as part of the type.

A value of type Fin n ranges from 0 to n - 1.

Operations that can cause numbers to be out-of-range come with variants that throw runtime errors, return Maybe, or return results modulo the bound.

In contrast to Data.Fin.Int, this module provides an API where runtime values of bound parameters are provided explicitly by SInts, which can be more intuitive than passing implicitly via KnownNat, and can avoid some runtime Natural-to-Int conversions and bounds checks resulting from KnownNat, at the cost of making some code more tedious where the bounds "should" be obvious.

Finite Natural Numbers

data Fin (n :: Nat)

Naturals bounded above by n.

Instances

FinSize n => Bounded (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

minBound :: Fin n

maxBound :: Fin n

KnownNat n => Enum (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

succ :: Fin n -> Fin n

pred :: Fin n -> Fin n

toEnum :: Int -> Fin n

fromEnum :: Fin n -> Int

enumFrom :: Fin n -> [Fin n]

enumFromThen :: Fin n -> Fin n -> [Fin n]

enumFromTo :: Fin n -> Fin n -> [Fin n]

enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n]

Eq (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

(==) :: Fin n -> Fin n -> Bool

(/=) :: Fin n -> Fin n -> Bool

KnownNat n => Data (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Fin n -> c (Fin n)

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Fin n)

toConstr :: Fin n -> Constr

dataTypeOf :: Fin n -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Fin n))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Fin n))

gmapT :: (forall b. Data b => b -> b) -> Fin n -> Fin n

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Fin n -> r

gmapQ :: (forall d. Data d => d -> u) -> Fin n -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Fin n -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Fin n -> m (Fin n)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Fin n -> m (Fin n)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Fin n -> m (Fin n)

Ord (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

compare :: Fin n -> Fin n -> Ordering

(<) :: Fin n -> Fin n -> Bool

(<=) :: Fin n -> Fin n -> Bool

(>) :: Fin n -> Fin n -> Bool

(>=) :: Fin n -> Fin n -> Bool

max :: Fin n -> Fin n -> Fin n

min :: Fin n -> Fin n -> Fin n

KnownNat n => Read (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

readsPrec :: Int -> ReadS (Fin n)

readList :: ReadS [Fin n]

readPrec :: ReadPrec (Fin n)

readListPrec :: ReadPrec [Fin n]

Show (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

FinSize n => Arbitrary (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

arbitrary :: Gen (Fin n)

shrink :: Fin n -> [Fin n]

KnownNat n => Default (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

def :: Fin n

NFData (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

rnf :: Fin n -> ()

Portray (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

portray :: Fin n -> Portrayal

Diff (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

diff :: Fin n -> Fin n -> Maybe Portrayal

type FinSize n = (KnownNat n, 1 <= n)

Constraint synonym for naturals n s.t. Fin n is inhabited.

Conversion

fin :: HasCallStack => SInt n -> Int -> Fin n

Construct a Fin from an Int, with bounds checks.

finFromIntegral :: (HasCallStack, Integral a, Show a) => SInt n -> a -> Fin n

This is similar to fromInteger, but you get a stack trace on error.

knownFin :: i <= (n - 1) => SInt i -> Fin n

Like fin, but doesn't do any bounds checks. However, unlike unsafeFin, this is safe (by virtue of the type constraints).

tryFin :: Integral a => SInt n -> a -> Maybe (Fin n)

Convert a number to a Fin, or Nothing if out of range.

finMod :: forall n a. (HasCallStack, Integral a) => SInt n -> a -> Fin n

finMod @n x is equivalent to fin @n (x mod (valueOf @n))

This raises an exception iff n ~ 0. It could have been written with a 0 < n constraint instead, but that would be annoying to prove repeatedly.

finDivMod :: forall n a. (HasCallStack, Integral a) => SInt n -> a -> (a, Fin n)

Decompose a number into a component modulo n and the rest.

This raises an exception iff n ~ 0. See finMod.

finToInt :: Fin n -> Int

This is like fromIntegral, but without the annoying context.

Bound Manipulation

embed :: m <= n => Fin m -> Fin n

Convert to a bigger type.

unembed :: HasCallStack => SInt n -> Fin m -> Fin n

Convert to a possibly smaller type. This function fails if the number is too big.

tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)

Convert to a possibly smaller type or return Nothing if out of bounds.

shiftFin :: SInt m -> Fin n -> Fin (m + n)

shiftFin increases the value and bound of a Fin both by m.

unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m + n) -> Fin n

unshiftFin decreases the value and bound of a Fin both by m.

tryUnshiftFin :: SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)

tryUnshiftFin decreases the value and bound of a Fin both by m.

splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)

Deconstructs the given Fin into one of two cases depending where it lies in the given range.

concatFin :: SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)

The inverse of splitFin.

weaken :: Fin n -> Fin (n + 1)

embed increasing the bound by exactly one.

strengthen :: SInt n -> Fin (n + 1) -> Maybe (Fin n)

Shrink the bound by one if possible.

Enumeration

minFin :: 1 <= n => Fin n

The minimal value of the given inhabited Fin type (i.e. 0).

maxFin :: 1 <= n => SInt n -> Fin n

The maximal value of the given inhabited Fin type (i.e n - 1).

enumFin :: SInt n -> [Fin n]

Enumerate the entire domain in ascending order. This is equivalent to enumFrom 0 or enumFrom minBound, but without introducing a spurious (1 <= n) constraint.

enumFinDown :: SInt n -> [Fin n]

Enumerate the entire domain in descending order. This is equivalent to reverse enumFin, but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

enumDownFrom :: SInt n -> Fin n -> [Fin n]

Equivalent to reverse (enumFromTo 0 x) but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

enumDownTo :: SInt n -> Fin n -> [Fin n]

Equivalent to reverse (enumFromTo x maxBound) but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]

Equivalent to reverse (enumFromTo y x) but without introducing a spurious (1 <= n) constraint or breaking list-fusion.

Arithmetic

In Maybe

tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)

Add, returning Nothing for out-of-range results.

trySub :: Fin n -> Fin n -> Maybe (Fin n)

Subtract, returning Nothing for out-of-range results.

tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)

Multiply, returning Nothing for out-of-range results.

Checked

chkAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n

Add and assert the result is in-range.

chkSub :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n

Subtract and assert the result is in-range.

chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n

Multiply and assert the result is in-range.

Modular arithmetic

modAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n

Add modulo n.

Raises error when intermediate results overflow Int.

modSub :: SInt n -> Fin n -> Fin n -> Fin n

Subtract modulo n.

modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n

Multiply modulo n.

Raises error when intermediate results overflow Int.

modNegate :: SInt n -> Fin n -> Fin n

Negate modulo n.

Compared to complementFin, this is shifted by 1: complementFin 0 :: Fin n = n - 1, while modNegate 0 :: Fin n = 0.

Miscellaneous

divModFin :: SInt m -> Fin (d * m) -> (Fin d, Fin m)

Split a Fin of the form d*x + y into (x, y).

complementFin :: SInt n -> Fin n -> Fin n

Reverse the order of the values of a Fin type.

twice :: SInt n -> Fin n -> Fin n

(*2), but works even if 2 is out-of-bounds.

half :: Fin n -> Fin n

Divide by 2, rounding down.

quarter :: Fin n -> Fin n

Divide by 4, rounding down.

crossFin :: SInt n -> Fin m -> Fin n -> Fin (m * n)

Given two Fins, returns one the size of the inputs' cartesian product.

The second argument is the lower-order one, i.e.

crossFin @_ @n (x+1) y = n + crossFin @_ @n x y
crossFin @_ @n x (y+1) = 1 + crossFin @_ @n x y

Attenuations

attLT :: n <= m => Attenuation (Fin n) (Fin m)

Restricted coercion to larger Fin types.

attPlus :: Attenuation (Fin n) (Fin (n + k))

Restricted coercion to larger Fin types.

attMinus :: Attenuation (Fin (n - k)) (Fin n)

Restricted coercion to larger Fin types.

attInt :: Attenuation (Fin n) Int

Restricted coercion to Int.

Unsafe, fast

unsafeFin :: Integral a => a -> Fin n

Like fin, but doesn't do any bounds checks.

unsafePred :: Fin n -> Fin n

Decrement by 1, without the validity checks of pred.

unsafeSucc :: Fin n -> Fin n

Increment by 1, without the validity checks of succ.

unsafeCoFin :: Coercion (Fin n) (Fin m)

Unsafe coercion between any Fin types.

unsafeCoInt :: Coercion (Fin n) Int

Unsafe coercion to and from Int.