parameterized-utils-2.1.11.0: Classes and data structures for working with data-kind indexed types

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
- 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
- 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)
- fin0Void :: Iso' (Fin 0) Void
- fin1Unit :: Iso' (Fin 1) ()
- fin2Bool :: Iso' (Fin 2) Bool

# 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 Source # maxBound :: Fin n Source #
Show (Fin n) Source # | Non-lawful instance, intended only for testing.
Instance details Defined in Data.Parameterized.Fin Methods showsPrec :: Int -> Fin n -> ShowS Source # show :: Fin n -> String Source # showList :: [Fin n] -> ShowS Source #
Eq (Fin n) Source # |
Instance details Defined in Data.Parameterized.Fin Methods (==) :: Fin n -> Fin n -> Bool Source # (/=) :: Fin n -> Fin n -> Bool Source #
Ord (Fin n) Source # |
Instance details Defined in Data.Parameterized.Fin Methods compare :: Fin n -> Fin n -> Ordering Source # (<) :: Fin n -> Fin n -> Bool Source # (<=) :: Fin n -> Fin n -> Bool Source # (>) :: Fin n -> Fin n -> Bool Source # (>=) :: Fin n -> Fin n -> Bool Source # max :: Fin n -> Fin n -> Fin n Source # min :: Fin n -> Fin n -> Fin n Source #
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 Source #

ifoldMap' :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m Source #

ifoldr :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b Source #

ifoldl :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b Source #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b Source #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b Source #

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 Source #

ifoldMap' :: Monoid m => (Fin n -> a -> m) -> FinMap n a -> m Source #

ifoldr :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b Source #

ifoldl :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b Source #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> FinMap n a -> b Source #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> FinMap n a -> b Source #

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 Source #

ifoldMap' :: Monoid m => (Fin n -> a -> m) -> Vector n a -> m Source #

ifoldr :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b Source #

ifoldl :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b Source #

ifoldr' :: (Fin n -> a -> b -> b) -> b -> Vector n a -> b Source #

ifoldl' :: (Fin n -> b -> a -> b) -> b -> Vector n a -> b Source #

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 Source #
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 Source #
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 Source #
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) Source #

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

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 #

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 #

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

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

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