| Copyright | (c) Artem Chirkin |
|---|---|
| License | BSD3 |
| Maintainer | chirkin@arch.ethz.ch |
| Safe Haskell | None |
| Language | Haskell2010 |
Numeric.Dimensions.Dims
Contents
Description
Provides a data type `Dims ds` to keep dimension sizes for multiple-dimensional data. Lower indices go first, i.e. assumed enumeration is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1).
- type Dims (xs :: [k]) = TypedList Dim xs
- data SomeDims = SomeDims (Dims ns)
- class Dimensions (ds :: [k]) where
- data TypedList (f :: k -> Type) (xs :: [k]) where
- pattern Dims :: forall ds. Dimensions ds => Dims ds
- pattern XDims :: forall (xns :: [XNat]). KnownXNatTypes xns => forall (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims ns -> Dims xns
- pattern AsXDims :: forall (ns :: [Nat]). (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns)) => Dims (AsXDims ns) -> Dims ns
- pattern KnownDims :: forall ds. (All KnownDim ds, Dimensions ds) => Dims ds
- pattern U :: forall (f :: k -> Type) (xs :: [k]). xs ~ '[] => TypedList f xs
- pattern (:*) :: forall (f :: k -> Type) (xs :: [k]). forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Empty :: forall (f :: k -> Type) (xs :: [k]). xs ~ '[] => TypedList f xs
- pattern TypeList :: forall (xs :: [k]). RepresentableList xs => TypeList xs
- pattern Cons :: forall (f :: k -> Type) (xs :: [k]). forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Snoc :: forall (f :: k -> Type) (xs :: [k]). forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
- pattern Reverse :: forall (f :: k -> Type) (xs :: [k]). forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => TypedList f sx -> TypedList f xs
- listDims :: Dims xs -> [Word]
- someDimsVal :: [Word] -> SomeDims
- totalDim :: Dims xs -> Word
- totalDim' :: forall xs. Dimensions xs => Word
- sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs))
- sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) p q. (Dimensions as, Dimensions bs) => p as -> q bs -> Maybe (Evidence (as ~ bs))
- compareDims :: Dims as -> Dims bs -> Ordering
- compareDims' :: forall as bs p q. (Dimensions as, Dimensions bs) => p as -> q bs -> Ordering
- inSpaceOf :: a ds -> b ds -> a ds
- asSpaceOf :: a ds -> (b ds -> c) -> b ds -> c
- xDims :: FixedDims xns ns => Dims ns -> Dims xns
- xDims' :: forall xns ns. (FixedDims xns ns, Dimensions ns) => Dims xns
- type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where ...
- type family AsDims (xns :: [XNat]) = (ns :: [Nat]) | ns -> xns where ...
- type family FixedDims (xns :: [XNat]) (ns :: [Nat]) :: Constraint where ...
- type KnownXNatTypes xns = All KnownXNatType xns
- type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where ...
- type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where ...
- class RepresentableList (xs :: [k]) where
- type TypeList (xs :: [k]) = TypedList Proxy xs
- types :: TypedList f xs -> TypeList xs
- order :: TypedList f xs -> Dim (Length xs)
- order' :: forall xs. RepresentableList xs => Dim (Length xs)
- module Numeric.Dim
Documentation
Same as SomeNat, but for Dimensions: Hide all information about Dimensions inside
class Dimensions (ds :: [k]) where Source #
Minimal complete definition
Methods
Get dimensionality of a space at runtime,
represented as a list of Dim.
Note, this function is supposed to be used with TypeApplications,
and the Dimensions class has varying kind of the parameter;
thus, the function has two type paremeters (kind and type of ds).
For example, you can type:
>>>:set -XTypeApplications>>>:set -XDataKinds>>>:t dims @_ @'[N 17, N 12]dims @_ @'[N 17, N 12] :: Dims '[N 17, N 12]
>>>:t dims @XNat @'[]dims @XNat @'[] :: Dims '[]
>>>:t dims @_ @(Tail '[3,2,5,7])dims @_ @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7]
Instances
| Dimensions k ([] k) Source # | |
| (KnownDim k d, Dimensions k ds) => Dimensions k ((:) k d ds) Source # | |
data TypedList (f :: k -> Type) (xs :: [k]) where Source #
Type-indexed list
Bundled Patterns
| pattern Dims :: forall ds. Dimensions ds => Dims ds |
|
| pattern XDims :: forall (xns :: [XNat]). KnownXNatTypes xns => forall (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims ns -> Dims xns | Pattern-matching against this constructor reveals Nat-kinded list of dims,
pretending the dimensionality is known at compile time within the scope
of the pattern match.
This is the main recommended way to get In order to use this pattern, one must know |
| pattern AsXDims :: forall (ns :: [Nat]). (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns)) => Dims (AsXDims ns) -> Dims ns | An easy way to convert Nat-indexed dims into XNat-indexed dims. |
| pattern KnownDims :: forall ds. (All KnownDim ds, Dimensions ds) => Dims ds |
|
| pattern U :: forall (f :: k -> Type) (xs :: [k]). xs ~ '[] => TypedList f xs | Zero-length type list |
| pattern (:*) :: forall (f :: k -> Type) (xs :: [k]). forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs infixr 5 | Constructing a type-indexed list |
| pattern Empty :: forall (f :: k -> Type) (xs :: [k]). xs ~ '[] => TypedList f xs | Zero-length type list; synonym to |
| pattern TypeList :: forall (xs :: [k]). RepresentableList xs => TypeList xs | Pattern matching against this causes |
| pattern Cons :: forall (f :: k -> Type) (xs :: [k]). forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs | Constructing a type-indexed list in the canonical way |
| pattern Snoc :: forall (f :: k -> Type) (xs :: [k]). forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs | Constructing a type-indexed list from the other end |
| pattern Reverse :: forall (f :: k -> Type) (xs :: [k]). forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => TypedList f sx -> TypedList f xs | Reverse a typed list |
Instances
| (RepresentableList * xs, All * Bounded xs) => Bounded (Tuple xs) # | |
| (RepresentableList * xs, All * Bounded xs) => Bounded (Tuple xs) # | |
| All * Eq xs => Eq (Tuple xs) # | |
| All * Eq xs => Eq (Tuple xs) # | |
| (All * Eq xs, All * Ord xs) => Ord (Tuple xs) # | Ord instance of the Tuple implements inverse lexicorgaphic ordering. That is, the last element in the tuple is the most significant one. Note, this will never work on infinite-dimensional tuples! |
| (All * Eq xs, All * Ord xs) => Ord (Tuple xs) # | Ord instance of the Tuple implements inverse lexicorgaphic ordering. That is, the last element in the tuple is the most significant one. Note, this will never work on infinite-dimensional tuples! |
| (RepresentableList * xs, All * Read xs) => Read (Tuple xs) # | |
| (RepresentableList * xs, All * Read xs) => Read (Tuple xs) # | |
| All * Show xs => Show (Tuple xs) # | |
| All * Show xs => Show (Tuple xs) # | |
| All * Semigroup xs => Semigroup (Tuple xs) # | |
| All * Semigroup xs => Semigroup (Tuple xs) # | |
| (Semigroup (Tuple xs), RepresentableList Type xs, All * Monoid xs) => Monoid (Tuple xs) # | |
| (Semigroup (Tuple xs), RepresentableList Type xs, All * Monoid xs) => Monoid (Tuple xs) # | |
| Dimensions k ds => Bounded (Idxs k ds) # | |
| Dimensions k ds => Enum (Idxs k ds) # | |
| Eq (Idxs k xs) # | |
| KnownDim k n => Num (Idxs k ((:) k n ([] k))) # | With this instance we can slightly reduce indexing expressions, e.g. x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U) |
| Ord (Idxs k xs) # | Compare indices by their importance in lexicorgaphic order
from the last dimension to the first dimension
(the last dimension is the most significant one) Literally, compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b) This is the same sort == sortOn fromEnum |
| Show (Idxs k xs) # | |
listDims :: Dims xs -> [Word] Source #
Convert `Dims xs` to a plain haskell list of dimension sizes O(1).
someDimsVal :: [Word] -> SomeDims Source #
Convert a plain haskell list of dimension sizes into an unknown
type-level dimensionality O(1).
totalDim' :: forall xs. Dimensions xs => Word Source #
Product of all dimension sizes O(Length xs).
sameDims :: Dims (as :: [Nat]) -> Dims (bs :: [Nat]) -> Maybe (Evidence (as ~ bs)) Source #
We either get evidence that this function was instantiated with the
same type-level Dimensions, or Nothing O(Length xs).
Note, this function works on Nat-indexed dimensions only,
because Dims '[XN x] does not have runtime evidence to infer x
and `KnownDim x` does not imply `KnownDim (XN x)`.
sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) p q. (Dimensions as, Dimensions bs) => p as -> q bs -> Maybe (Evidence (as ~ bs)) Source #
We either get evidence that this function was instantiated with the
same type-level Dimensions, or Nothing O(Length xs).
compareDims :: Dims as -> Dims bs -> Ordering Source #
Compare dimensions by their size in lexicorgaphic order from the last dimension to the first dimension (the last dimension is the most significant one).
Literally,
compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)
compareDims' :: forall as bs p q. (Dimensions as, Dimensions bs) => p as -> q bs -> Ordering Source #
Compare dimensions by their size in lexicorgaphic order
from the last dimension to the first dimension
(the last dimension is the most significant one) O(Length xs).
Literally,
compareDims a b = compare (reverse $ listDims a) (reverse $ listDims b)
This is the same compare rule, as for Idxs.
asSpaceOf :: a ds -> (b ds -> c) -> b ds -> c Source #
Similar to asProxyTypeOf,
Give a hint to type checker to fix the type of a function argument.
xDims :: FixedDims xns ns => Dims ns -> Dims xns Source #
Get XNat-indexed dims given their fixed counterpart.
xDims' :: forall xns ns. (FixedDims xns ns, Dimensions ns) => Dims xns Source #
Get XNat-indexed dims given their fixed counterpart.
Type-level programming
type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where ... Source #
Map Dims onto XDims (injective)
type family AsDims (xns :: [XNat]) = (ns :: [Nat]) | ns -> xns where ... Source #
Map XDims onto Dims (injective)
type family FixedDims (xns :: [XNat]) (ns :: [Nat]) :: Constraint where ... Source #
Constrain Nat dimensions hidden behind XNats.
type KnownXNatTypes xns = All KnownXNatType xns Source #
Know the structure of each dimension
type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where ... infixr 6 Source #
Synonym for (:+) that treats Nat values 0 and 1 in a special way: it preserves the property that all dimensions are greater than 1.
type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where ... infixl 6 Source #
Synonym for (+:) that treats Nat values 0 and 1 in a special way: it preserves the property that all dimensions are greater than 1.
Re-export type list
class RepresentableList (xs :: [k]) where Source #
Representable type lists. Allows getting type information about list structure at runtime.
Minimal complete definition
Instances
| RepresentableList k ([] k) Source # | |
| RepresentableList k xs => RepresentableList k ((:) k x xs) Source # | |
types :: TypedList f xs -> TypeList xs Source #
Get a constructible TypeList from any other TypedList;
Pattern matching agains the result brings RepresentableList constraint
into the scope:
case types ts of TypeList -> ...
Re-export single dimension type and functions
module Numeric.Dim