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
mkFin :: forall i n. (i + 1) <= n => NatRepr i -> Fin n
buildFin :: forall m. NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Fin ((n + 1) + 1)) -> Fin (m + 1)
countFin :: NatRepr m -> (forall n. (n + 1) <= m => NatRepr n -> Fin (n + 1) -> Bool) -> Fin (m + 1)
viewFin :: (forall i. (i + 1) <= n => NatRepr i -> r) -> Fin n -> r
finToNat :: Fin n -> Natural
embed :: forall n m. n <= m => Fin n -> Fin m
tryEmbed :: NatRepr n -> NatRepr m -> Fin n -> Maybe (Fin m)
minFin :: 1 <= n => Fin n
incFin :: forall n. Fin n -> Fin (n + 1)
fin0Void :: Iso' (Fin 0) Void
fin1Unit :: Iso' (Fin 1) ()
fin2Bool :: Iso' (Fin 2) Bool

Documentation

data Fin n 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 #
Show (Fin n) Source #	Non-lawful instance, intended only for testing.
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 #
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 n. (i + 1) <= n => NatRepr i -> Fin n Source #

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

countFin :: NatRepr m -> (forall n. (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 i. (i + 1) <= n => NatRepr i -> r) -> Fin n -> r Source #

finToNat :: Fin n -> Natural Source #

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

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

minFin :: 1 <= n => Fin n Source #

The smallest element of Fin n

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

fin0Void :: Iso' (Fin 0) Void Source #

fin1Unit :: Iso' (Fin 1) () Source #

fin2Bool :: Iso' (Fin 2) Bool Source #