Copyright	(c) Galois Inc 2021
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Parameterized.Fin

Description

Fin n is a finite type with exactly n elements. Essentially, they bundle a NatRepr that has an existentially-quantified type parameter with a proof that its parameter is less than some fixed natural.

They are useful in combination with types of a fixed size. For example Fin is used as the index in the FunctorWithIndex instance for Vector. As another example, a Map (Fin n) a is a Map that naturally has a fixed size bound of n.

Synopsis

data Fin (n :: Natural)
mkFin :: forall (i :: Natural) (n :: Natural). (i + 1) <= n => NatRepr i -> Fin n
mkFinModN :: forall (n :: Natural) (i :: Nat). 1 <= n => NatRepr n -> NatRepr i -> Fin n
buildFin :: forall (m :: Nat). NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)) -> Fin (m + 1)
countFin :: forall (m :: Nat). NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Bool) -> Fin (m + 1)
viewFin :: forall (n :: Natural) r. (forall (i :: Natural). (i + 1) <= n => NatRepr i -> r) -> Fin n -> r
finFromNatModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Natural -> Fin n
finToNat :: forall (n :: Natural). Fin n -> Natural
embed :: forall (n :: Natural) (m :: Natural). n <= m => Fin n -> Fin m
tryEmbed :: forall (n :: Nat) (m :: Nat). NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
minFin :: forall (n :: Natural). 1 <= n => Fin n
incFin :: forall (n :: Natural). Fin n -> Fin (n + 1)
fin0Absurd :: Fin 0 -> a
addFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n -> Fin n
subFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n -> Fin n
mulFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n -> Fin n
negFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n
recipFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Maybe (Fin n)

Documentation

data Fin (n :: Natural) Source #

The type Fin n has exactly n inhabitants.

Instances

Instances details

(1 <= n, KnownNat n) => Bounded (Fin n) Source #
Instance details Defined in Data.Parameterized.Fin Methods minBound :: Fin n # maxBound :: Fin n #
(1 <= n, KnownNat n) => Num (Fin n) Source #	Arithmetic is performed modulo `n`.
Instance details Defined in Data.Parameterized.Fin Methods (+) :: Fin n -> Fin n -> Fin n # (-) :: Fin n -> Fin n -> Fin n # (*) :: Fin n -> Fin n -> Fin n # negate :: Fin n -> Fin n # abs :: Fin n -> Fin n # signum :: Fin n -> Fin n # fromInteger :: Integer -> Fin n #
Show (Fin n) Source #
Instance details Defined in Data.Parameterized.Fin Methods showsPrec :: Int -> Fin n -> ShowS # show :: Fin n -> String # showList :: [Fin n] -> ShowS #
Eq (Fin n) Source #
Instance details Defined in Data.Parameterized.Fin Methods (==) :: Fin n -> Fin n -> Bool # (/=) :: Fin n -> Fin n -> Bool #
Ord (Fin n) Source #
Instance details Defined in Data.Parameterized.Fin 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 #
Hashable (Fin n) Source #
Instance details Defined in Data.Parameterized.Fin Methods hashWithSalt :: Int -> Fin n -> Int # hash :: Fin n -> Int #
FoldableWithIndex (Fin n) (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b #
FoldableWithIndex (Fin n) (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Unsafe Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b #
FoldableWithIndex (Fin n) (Vector n) Source #
Instance details Defined in Data.Parameterized.Vector Methods ifoldMap :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m # ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m # ifoldr :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b # ifoldl :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b # ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b # ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b #
FunctorWithIndex (Fin n) (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Safe Methods imap :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b #
FunctorWithIndex (Fin n) (FinMap n) Source #
Instance details Defined in Data.Parameterized.FinMap.Unsafe Methods imap :: (Fin n -> a -> b) -> FinMap n a -> FinMap n b #
FunctorWithIndex (Fin n) (Vector n) Source #
Instance details Defined in Data.Parameterized.Vector Methods imap :: (Fin n -> a -> b) -> Vector n a -> Vector n b #
TraversableWithIndex (Fin n) (Vector n) Source #
Instance details Defined in Data.Parameterized.Vector Methods itraverse :: Applicative f => (Fin n -> a -> f b) -> Vector n a -> f (Vector n b) #

mkFin :: forall (i :: Natural) (n :: Natural). (i + 1) <= n => NatRepr i -> Fin n Source #

mkFinModN :: forall (n :: Natural) (i :: Nat). 1 <= n => NatRepr n -> NatRepr i -> Fin n Source #

Construct a Fin n value from the number i, where i is reduced modulo n.

buildFin :: forall (m :: Nat). NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)) -> Fin (m + 1) Source #

countFin :: forall (m :: Nat). NatRepr m -> (forall (n :: Natural). (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Bool) -> Fin (m + 1) Source #

Count all of the numbers up to m that meet some condition.

viewFin :: forall (n :: Natural) r. (forall (i :: Natural). (i + 1) <= n => NatRepr i -> r) -> Fin n -> r Source #

finFromNatModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Natural -> Fin n Source #

Construct a Fin n value from a Natural input, where the input is reduced modulo n.

finToNat :: forall (n :: Natural). Fin n -> Natural Source #

embed :: forall (n :: Natural) (m :: Natural). n <= m => Fin n -> Fin m Source #

tryEmbed :: forall (n :: Nat) (m :: Nat). NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m) Source #

minFin :: forall (n :: Natural). 1 <= n => Fin n Source #

The smallest element of Fin n

incFin :: forall (n :: Natural). Fin n -> Fin (n + 1) Source #

fin0Absurd :: Fin 0 -> a Source #

It is not possible to construct an element of Fin 0.

addFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n -> Fin n Source #

Add two Fin n values and reduce the result modulo n.

subFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n -> Fin n Source #

Subtract two Fin n values and reduce the result modulo n.

mulFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n -> Fin n Source #

Multiply two Fin n values and reduce the result modulo n.

negFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Fin n Source #

Given a value i :: Fin n value, negate it. That is, if i is zero, then return i unchanged, and if i is non-zero, then compute n - i. This is a negation in the sense that it is an additive inverse: adding i to its negation will yield minFin.

recipFinModN :: forall (n :: Natural). 1 <= n => NatRepr n -> Fin n -> Maybe (Fin n) Source #

Given a value i :: Fin n, compute the reciprocal (i.e., the modular inverse) if one exists. That is, attempt to compute i^-1 such that i * i^-1 equals 1 modulo n. Note that a reciprocal will only exist if i and n are relatively prime, i.e., if gcd i n == 1. If they are not relatively prime, then this function will return Nothing.

Note that in the degenerate case where n == 1, this function will always return Just 0. The value 0 is the only element of Fin 1, and 0 is its own reciprocal.