Data.Microgroove.Index

Prepared Indicies into a Record

newtype Index (xs :: [u]) (x :: u)

A prepared index into a record, allowing fast access

Constructors

Index# Int

Bundled Patterns

pattern RZ :: Index (x ': xs) (x :: u)

Construct or pattern match the zero index, refining its type

pattern RS :: Index (xs :: [u]) (x :: u) -> Index (y ': xs) x

Construct or pattern match a successor index, refining its type

Instances

Show (Index u xs x)

Methods

showsPrec :: Int -> Index u xs x -> ShowS

show :: Index u xs x -> String

showList :: [Index u xs x] -> ShowS

Constructing Indicies

mkIndex :: forall n xs. (KnownNat n, n <= (Length xs - 1)) => Index xs (xs !! n)

Construct a statically known index into a record. O(1)

checkIndex :: forall (xs :: [*]). KnownNat (Length xs) => Int -> MaybeSome (Index xs)

Prepare a dynamically known index into a statically known record. O(n) and better constants than checkIndex'

checkIndex' :: forall (xs :: [u]). KnownNat (Length xs) => Int -> MaybeSome (Index xs)

Prepare a dynamically known index into a statically known record. Like checkIndex but polykinded O(n) and better constants than checkIndex'