Data.Fin.Int

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.Explicit, this module provides an API that accepts the bounds values implicitly via KnownNat. This can be more convenient when there's no arithmetic involved in the bounds, but may cost more runtime Natural-to-Int conversions.

When type-level arithmetic is involved, the ghc-typelits-knownnat plugin may be useful to derive KnownNat instances for bounds automatically.

Finite Natural Numbers

data Fin (n :: Nat)

Naturals bounded above by n.

Instances

FinSize n => Arbitrary (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

arbitrary :: Gen (Fin n)

shrink :: Fin n -> [Fin n]

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)

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]

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

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 -> ()

Eq (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

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

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

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

Portray (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

portray :: Fin n -> Portrayal

portrayList :: [Fin n] -> Portrayal

Diff (Fin n)

Defined in Data.Fin.Int.Explicit

Methods

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

Attenuable (Fin n :: TYPE LiftedRep) Int

Defined in Data.Fin.Int.Explicit

Methods

attenuation :: Attenuation (Fin n) Int

m <= n => Attenuable (Fin m :: TYPE LiftedRep) (Fin n :: TYPE LiftedRep)

Defined in Data.Fin.Int.Explicit

Methods

attenuation :: Attenuation (Fin m) (Fin n)

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

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

Conversion

fin :: forall n. (HasCallStack, KnownNat n) => Int -> Fin n

Construct a Fin from an Int, with bounds checks.

finFromIntegral :: forall n a. (HasCallStack, KnownNat n, Integral a, Show a) => a -> Fin n

Generalized fin that works on any Integral type.

knownFin :: forall i n. (KnownNat i, i <= (n - 1)) => Fin n

Construct a Fin from a Nat known to be in-bounds.

tryFin :: forall n a. (Integral a, KnownNat n) => a -> Maybe (Fin n)

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

finMod :: forall n a. (HasCallStack, Integral a, KnownNat 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, KnownNat 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

Convert a Fin to the underlying Int representing it.

Bound Manipulation

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

Convert to a Fin with a larger bound.

This is equivalent to a specialization of attenuate.

unembed :: (HasCallStack, KnownNat n) => Fin m -> Fin n

Convert to a Fin with a (potentially) smaller bound.

This function throws an exception if the number is out of range of the target type.

tryUnembed :: KnownNat n => Fin m -> Maybe (Fin n)

Convert to a Fin with a (potentially) smaller bound.

Returns Nothing if the number is out of range of the target type.

shiftFin :: forall m n. KnownNat m => Fin n -> Fin (m + n)

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

unshiftFin :: forall m n. (HasCallStack, KnownNat m, KnownNat n) => Fin (m + n) -> Fin n

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

Raises an exception if the result would be negative.

tryUnshiftFin :: forall m n. (KnownNat m, KnownNat n) => Fin (m + n) -> Maybe (Fin n)

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

splitFin :: forall m n. KnownNat 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 :: forall m n. KnownNat 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 :: forall n. KnownNat 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, KnownNat n) => Fin n

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

enumFin :: forall n. KnownNat 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 :: forall n. KnownNat 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 :: forall n. KnownNat n => Fin n -> [Fin n]

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

enumDownTo :: forall n. KnownNat n => Fin n -> [Fin n]

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

enumDownFromTo :: forall n. KnownNat 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 :: KnownNat 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 :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)

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

(+?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)

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

(-?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)

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

(*?) :: KnownNat n => Fin n -> Fin n -> Maybe (Fin n)

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

Checked

chkAdd :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Add and assert the result is in-range.

chkAdd and (+!) are different names for the same function.

chkSub :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Subtract and assert the result is in-range.

chkSub and (-!) are different names for the same function.

chkMul :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Multiply and assert the result is in-range.

chkMul and (*!) are different names for the same function.

(+!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Add and assert the result is in-range.

chkAdd and (+!) are different names for the same function.

(-!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Subtract and assert the result is in-range.

chkSub and (-!) are different names for the same function.

(*!) :: (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Multiply and assert the result is in-range.

chkMul and (*!) are different names for the same function.

Modular arithmetic

modAdd :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Add modulo n.

Raises error when intermediate results overflow Int.

modAdd and (+%) are different names for the same function.

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

Subtract modulo n.

modMul :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Multiply modulo n.

Raises error when intermediate results overflow Int.

modMul and (*%) are different names for the same function.

modNegate :: forall n. KnownNat 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.

(+%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Add modulo n.

Raises error when intermediate results overflow Int.

modAdd and (+%) are different names for the same function.

(-%) :: forall n. KnownNat n => Fin n -> Fin n -> Fin n

Subtract modulo n.

modSub and (-%) are different names for the same function.

(*%) :: forall n. (HasCallStack, KnownNat n) => Fin n -> Fin n -> Fin n

Multiply modulo n.

Raises error when intermediate results overflow Int.

modMul and (*%) are different names for the same function.

Miscellaneous

divModFin :: forall m d. KnownNat m => Fin (d * m) -> (Fin d, Fin m)

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

complementFin :: forall n. KnownNat n => Fin n -> Fin n

Reverse the order of the values of a Fin type.

twice :: KnownNat 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 :: forall m n. KnownNat 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.

This is also available as an Attenuable instance.

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.

This is also available as an Attenuable instance.

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.