Safe Haskell | None |
---|---|
Language | Haskell2010 |
Finite natural numbers, with upper bound as part of the type.
A value of type
ranges from Fin
n0
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 SInt
s, 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.
Synopsis
- data Fin (n :: Nat)
- type FinSize n = (KnownNat n, 1 <= n)
- fin :: HasCallStack => SInt n -> Int -> Fin n
- finFromIntegral :: (HasCallStack, Integral a, Show a) => SInt n -> a -> Fin n
- knownFin :: i <= (n - 1) => SInt i -> Fin n
- tryFin :: Integral a => SInt n -> a -> Maybe (Fin n)
- finMod :: forall n a. (HasCallStack, Integral a) => SInt n -> a -> Fin n
- finDivMod :: forall n a. (HasCallStack, Integral a) => SInt n -> a -> (a, Fin n)
- finToInt :: Fin n -> Int
- embed :: m <= n => Fin m -> Fin n
- unembed :: HasCallStack => SInt n -> Fin m -> Fin n
- tryUnembed :: SInt n -> Fin m -> Maybe (Fin n)
- shiftFin :: SInt m -> Fin n -> Fin (m + n)
- unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m + n) -> Fin n
- tryUnshiftFin :: SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n)
- splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n)
- concatFin :: SInt m -> Either (Fin m) (Fin n) -> Fin (m + n)
- weaken :: Fin n -> Fin (n + 1)
- strengthen :: SInt n -> Fin (n + 1) -> Maybe (Fin n)
- minFin :: 1 <= n => Fin n
- maxFin :: 1 <= n => SInt n -> Fin n
- enumFin :: SInt n -> [Fin n]
- enumFinDown :: SInt n -> [Fin n]
- enumDownFrom :: SInt n -> Fin n -> [Fin n]
- enumDownTo :: SInt n -> Fin n -> [Fin n]
- enumDownFromTo :: SInt n -> Fin n -> Fin n -> [Fin n]
- tryAdd :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
- trySub :: Fin n -> Fin n -> Maybe (Fin n)
- tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n)
- chkAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
- chkSub :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
- chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
- modAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
- modSub :: SInt n -> Fin n -> Fin n -> Fin n
- modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n
- modNegate :: SInt n -> Fin n -> Fin n
- divModFin :: SInt m -> Fin (d * m) -> (Fin d, Fin m)
- complementFin :: SInt n -> Fin n -> Fin n
- twice :: SInt n -> Fin n -> Fin n
- half :: Fin n -> Fin n
- quarter :: Fin n -> Fin n
- crossFin :: SInt n -> Fin m -> Fin n -> Fin (m * n)
- attLT :: n <= m => Attenuation (Fin n) (Fin m)
- attPlus :: Attenuation (Fin n) (Fin (n + k))
- attMinus :: Attenuation (Fin (n - k)) (Fin n)
- attInt :: Attenuation (Fin n) Int
- unsafeFin :: Integral a => a -> Fin n
- unsafePred :: Fin n -> Fin n
- unsafeSucc :: Fin n -> Fin n
- unsafeCoFin :: Coercion (Fin n) (Fin m)
- unsafeCoInt :: Coercion (Fin n) Int
Finite Natural Numbers
Naturals bounded above by n
.
Instances
FinSize n => Bounded (Fin n) Source # | |
KnownNat n => Enum (Fin n) Source # | |
Eq (Fin n) Source # | |
KnownNat n => Data (Fin n) Source # | |
Defined in Data.Fin.Int.Explicit 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) # 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) Source # | |
KnownNat n => Read (Fin n) Source # | |
Show (Fin n) Source # | |
FinSize n => Arbitrary (Fin n) Source # | |
KnownNat n => Default (Fin n) Source # | |
Defined in Data.Fin.Int.Explicit | |
NFData (Fin n) Source # | |
Defined in Data.Fin.Int.Explicit | |
Portray (Fin n) Source # | |
Defined in Data.Fin.Int.Explicit | |
Diff (Fin n) Source # | |
Attenuable (Fin n :: Type) Int Source # | |
Defined in Data.Fin.Int.Explicit attenuation :: Attenuation (Fin n) Int # | |
m <= n => Attenuable (Fin m :: Type) (Fin n :: Type) Source # | |
Defined in Data.Fin.Int.Explicit attenuation :: Attenuation (Fin m) (Fin n) # |
type FinSize n = (KnownNat n, 1 <= n) Source #
Constraint synonym for naturals n
s.t.
is inhabited.Fin
n
Conversion
finFromIntegral :: (HasCallStack, Integral a, Show a) => SInt n -> a -> Fin n Source #
tryFin :: Integral a => SInt n -> a -> Maybe (Fin n) Source #
Convert a number to a Fin
, or Nothing
if out of range.
finMod :: forall n a. (HasCallStack, Integral a) => SInt n -> a -> Fin n Source #
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) Source #
Decompose a number into a component modulo n
and the rest.
This raises an exception iff n ~ 0
. See finMod
.
Bound Manipulation
unembed :: HasCallStack => SInt n -> Fin m -> Fin n Source #
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.
shiftFin :: SInt m -> Fin n -> Fin (m + n) Source #
shiftFin
increases the value and bound of a Fin both by m
.
unshiftFin :: HasCallStack => SInt m -> SInt n -> Fin (m + n) -> Fin n Source #
unshiftFin
decreases the value and bound of a Fin both by m
.
Raises an exception if the result would be negative.
tryUnshiftFin :: SInt m -> SInt n -> Fin (m + n) -> Maybe (Fin n) Source #
tryUnshiftFin
decreases the value and bound of a Fin both by m
.
splitFin :: SInt m -> Fin (m + n) -> Either (Fin m) (Fin n) Source #
Deconstructs the given Fin into one of two cases depending where it lies in the given range.
Enumeration
maxFin :: 1 <= n => SInt n -> Fin n Source #
The maximal value of the given inhabited Fin
type (i.e n - 1
).
enumFin :: SInt n -> [Fin n] Source #
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] Source #
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] Source #
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] Source #
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] Source #
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) Source #
Add, returning Nothing for out-of-range results.
trySub :: Fin n -> Fin n -> Maybe (Fin n) Source #
Subtract, returning Nothing for out-of-range results.
tryMul :: SInt n -> Fin n -> Fin n -> Maybe (Fin n) Source #
Multiply, returning Nothing for out-of-range results.
Checked
chkAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n Source #
Add and assert the result is in-range.
chkSub :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n Source #
Subtract and assert the result is in-range.
chkMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n Source #
Multiply and assert the result is in-range.
Modular arithmetic
modAdd :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n Source #
Add modulo n.
Raises error when intermediate results overflow Int.
modMul :: HasCallStack => SInt n -> Fin n -> Fin n -> Fin n Source #
Multiply modulo n.
Raises error when intermediate results overflow Int.
modNegate :: SInt n -> Fin n -> Fin n Source #
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) Source #
Split a Fin
of the form d*x + y
into (x, y)
.
crossFin :: SInt n -> Fin m -> Fin n -> Fin (m * n) Source #
Given two Fin
s, 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) Source #
Restricted coercion to larger Fin types.
This is also available as an Attenuable
instance.
attInt :: Attenuation (Fin n) Int Source #
Restricted coercion to Int.
This is also available as an Attenuable
instance.