Data.Parameterized.Fin

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.

Documentation

data Fin n

The type Fin n has exactly n inhabitants.

Instances

(1 <= n, KnownNat n) => Bounded (Fin n)

Defined in Data.Parameterized.Fin

Methods

minBound :: Fin n

maxBound :: Fin n

Eq (Fin n)

Defined in Data.Parameterized.Fin

Methods

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

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

Ord (Fin n)

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

Show (Fin n)

Non-lawful instance, intended only for testing.

Defined in Data.Parameterized.Fin

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

FunctorWithIndex (Fin n) (Vector n)

Defined in Data.Parameterized.Vector

Methods

imap :: (Fin n -> a -> b) -> Vector n a -> Vector n b

FoldableWithIndex (Fin n) (Vector n)

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

TraversableWithIndex (Fin n) (Vector n)

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

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

The smallest element of Fin n

fin0Void :: Iso' (Fin 0) Void

fin1Unit :: Iso' (Fin 1) ()

fin2Bool :: Iso' (Fin 2) Bool