dimensions-2.1.1.0: Safe type-level dimensionality for multidimensional data.

Numeric.Dimensions.Idx

Description

Provides a data type Idx to index Dim and Idxs that enumerates through multiple dimensions.

Higher indices go first, i.e. assumed enumeration is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik This corresponds to row-first layout of matrices and multidimenional arrays.

Type safety

Same as Dim and Dims, Idx and Idxs defined in this module incorporate two different indexing mechanics. Both of them can be specified with exact Nat values (when d :: Nat or d ~ N n), or with lower bound values (i.e. d ~ XN m). In the former case, the Idx/Idxs type itself guarantees that the value inside is within the Dim/Dims bounds. In the latter case, Idx/Idxs can contain any values of type Word. In other words:

• (d :: Nat) || (d ~ N n) => using Idx d to index data is always safe, but creating an index using unsafe functions can yield an OutOfDimBounds exception at runtime.
• (d ~ XN m) => using Idx d to index data can result in an OutOfDimBounds exception, but you can safely manipulate the index itself using familiar interfaces, such as Enum, Num, etc; as if Idx d was a plain synonym to Word.
Synopsis

Data types

data Idx (d :: k) where Source #

This type is used to index a single dimension.

• (k ~ Nat) => the range of indices is from 0 to d-1.
• (d ~ N n) => the range of indices is from 0 to n-1.
• (d ~ XN m) => the range of indices is from 0 to maxBound :: Word.

That is, using Idx (n :: Nat) or Idx (N n) is guaranteed to be safe by the type system. But an index of type Idx (XN m) can have any value, and using it may yield an OutOfDimBounds exception -- just the same as a generic index function that takes a plain Int or Word as an argument. Thus, if you have data indexed by (XN m), I would suggest to use lookup-like functions that return Maybe. You're warned.

Bundled Patterns

 pattern Idx :: forall d. BoundedDim d => Word -> Idx d Convert between Word and Idx.Converting from Idx to Word is always safe.Converting from Word to Idx generally is unsafe:(k ~ Nat) => if w >= d, it fails with an OutOfDimBounds exception.(d ~ N n) => if w >= n, it fails with an OutOfDimBounds exception.(d ~ XN m) => the constructor always succeeds, but using the result for indexing may fail with an OutOfDimBounds exception later.If unsafeindices flag it turned on, this function always succeeds.

Instances

Instances details

type Idxs = TypedList Idx :: [k] -> Type Source #

Type-level dimensional indexing with arbitrary Word values inside. Most of the operations on it require Dimensions or BoundedDims constraint, because the Idxs itself does not store info about dimension bounds.

idxFromWord :: forall d. BoundedDim d => Word -> Maybe (Idx d) Source #

Convert an arbitrary Word to Idx. This is a safe alternative to the pattern Idx.

Note, when (d ~ XN m), it returns Nothing if w >= m. Thus, the resulting index is always safe to use (but you cannot index stuff beyond DimBound d this way).

idxToWord :: forall d. Idx d -> Word Source #

Get the value of an Idx.

listIdxs :: forall ds. Idxs ds -> [Word] Source #

O(1) Convert Idxs xs to a plain list of words.

idxsFromWords :: forall ds. BoundedDims ds => [Word] -> Maybe (Idxs ds) Source #

O(n) Convert a plain list of words into an Idxs, while checking the index bounds.

Same as with idxFromWord, it is always safe to use the resulting index, but you cannot index stuff outside of the DimsBound ds this way.

liftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). FixedDims ds ns => Idxs ns -> Idxs ds Source #

O(1) Coerce a Nat-indexed list of indices into a XNat-indexed one. This function does not need any runtime checks and thus runs in constant time.

unliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). (FixedDims ds ns, Dimensions ns) => Idxs ds -> Maybe (Idxs ns) Source #

O(n) Coerce a XNat-indexed list of indices into a Nat-indexed one. This function checks if an index is within Dim bounds for every dimension.

unsafeUnliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). (FixedDims ds ns, Dimensions ns) => Idxs ds -> Idxs ns Source #

Coerce a XNat-indexed list of indices into a Nat-indexed one. Can throw an OutOfDimBounds exception unless unsafeindices flag is active.

data TypedList (f :: k -> Type) (xs :: [k]) where Source #

Type-indexed list

Bundled Patterns

 pattern XIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). (FixedDims ds ns, Dimensions ns) => Idxs ns -> Idxs ds Transform between Nat-indexed and XNat-indexed Idxs.Note, this pattern is not a COMPLETE match, because converting from XNat to Nat indexed Idxs may fail (see unliftIdxs). pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs Zero-length type list pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs infixr 5 Constructing a type-indexed list pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs Zero-length type list; synonym to U. pattern Cons :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs Constructing a type-indexed list in the canonical way pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs Constructing a type-indexed list from the other end pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs Reverse a typed list

Instances

Instances details

Checking the index bounds

Typically, this exception can occur in the following cases:

• Converting from integral values to Idx d when d ~ N n or d :: Nat.
• Using Enum and Num when d ~ N n or d :: Nat.
• Converting from Idx (XN m :: XNat) to Idx (n :: Nat).
• Indexing or slicing data using Idx (XN m :: XNat).

If you are mad and want to avoid any overhead related to bounds checking and the related error handling, you can turn on the unsafeindices flag to remove all of this from the library at once.

Constructors

 OutOfDimBounds FieldsoodIdx :: IntegerA value that should have been a valid IdxoodDim :: WordA runtime value of a DimoodSubDim :: Maybe WordWhen used for slicing, this should have satisfied oodIdx + oodSubDim <= oodDim.oodDimsCtx :: Maybe ([Word], [Word])If available, contains (Dims xns, Idxs xns).oodName :: StringShort description of the error location, typically a function name.oodCallStack :: Maybe CallStackFunction call stack, if available. Note, this field is ignored in the Eq and Ord instances.

Instances

Instances details
 Source # Note, this instance ignores oodCallStack Instance detailsDefined in Numeric.Dimensions.Idx Methods Source # Note, this instance ignores oodCallStack Instance detailsDefined in Numeric.Dimensions.Idx Methods Source # Instance detailsDefined in Numeric.Dimensions.Idx MethodsshowList :: [OutOfDimBounds] -> ShowS # Source # Instance detailsDefined in Numeric.Dimensions.Idx Methods

Arguments

 :: (HasCallStack, Integral i) => String Label (e.g. function name) -> i Bad index -> Word Target dim -> Maybe Word SubSpace Dim, if applicable. -> Maybe ([Word], [Word]) Larger picture: Dims and Idxs -> a

Throw an OutOfDimBounds exception.

Arguments

 :: Integral i => String Label (e.g. function name) -> i Bad index -> Word Target dim -> Maybe Word SubSpace Dim, if applicable. -> Maybe ([Word], [Word]) Larger picture: Dims and Idxs -> a

Throw an OutOfDimBounds exception without the CallStack attached.