| 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).
Synopsis
- type Dims (xs :: [k]) = TypedList Dim xs
- data SomeDims = SomeDims (Dims ns)
- class Dimensions (ds :: [k]) where
- class KnownXNatTypes xds => XDimensions (xds :: [XNat]) 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 #
Put runtime evidence of Dims value inside function constraints.
Similar to KnownDim or KnownNat, but for lists of numbers.
Normally, the kind paramater is Nat (known dimenionality)
or XNat (either known or constrained dimensionality).
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]) Source # | |
Defined in Numeric.Dimensions.Dims | |
| (KnownDim d, Dimensions ds) => Dimensions (d ': ds :: [k]) Source # | |
Defined in Numeric.Dimensions.Dims | |
class KnownXNatTypes xds => XDimensions (xds :: [XNat]) where Source #
Analogous to Dimensions, but weaker and more specific (list of XNat).
This class is used to check if an existing fixed Dims satisfy
constraints imposed by some interface (e.g. all dimensions are greater than 2).
It is weaker than Dimensions in that it only requires knowledge of constraints
rather than exact dimension values.
Minimal complete definition
Instances
| XDimensions ([] :: [XNat]) Source # | |
Defined in Numeric.Dimensions.Dims | |
| (XDimensions xs, KnownDim n) => XDimensions (N n ': xs) Source # | |
Defined in Numeric.Dimensions.Dims | |
| (XDimensions xs, KnownDim m) => XDimensions (XN m ': xs) Source # | |
Defined in Numeric.Dimensions.Dims | |
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! |
Defined in Numeric.Tuple.Strict | |
| (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! |
Defined in Numeric.Tuple.Lazy | |
| (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 xs, All Monoid xs) => Monoid (Tuple xs) # | |
| (Semigroup (Tuple xs), RepresentableList xs, All Monoid xs) => Monoid (Tuple xs) # | |
| Dimensions ds => Bounded (Dims ds) # | |
| Dimensions ds => Bounded (Idxs ds) # | |
| Dimensions ds => Enum (Idxs ds) # | |
| Eq (Dims ds) # | |
| Eq (Dims ds) # | |
| Eq (Idxs xs) # | |
| KnownDim n => Num (Idxs (n ': ([] :: [k]))) # | With this instance we can slightly reduce indexing expressions, e.g. x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U) |
Defined in Numeric.Dimensions.Idxs Methods (+) :: Idxs (n ': []) -> Idxs (n ': []) -> Idxs (n ': []) # (-) :: Idxs (n ': []) -> Idxs (n ': []) -> Idxs (n ': []) # (*) :: Idxs (n ': []) -> Idxs (n ': []) -> Idxs (n ': []) # negate :: Idxs (n ': []) -> Idxs (n ': []) # abs :: Idxs (n ': []) -> Idxs (n ': []) # signum :: Idxs (n ': []) -> Idxs (n ': []) # fromInteger :: Integer -> Idxs (n ': []) # | |
| Ord (Dims ds) # | |
Defined in Numeric.Dimensions.Dims | |
| Ord (Dims ds) # | |
Defined in Numeric.Dimensions.Dims | |
| Ord (Idxs 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 |
Defined in Numeric.Dimensions.Idxs | |
| Show (Dims xs) # | |
| Show (Idxs 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]) Source # | |
Defined in Numeric.TypedList | |
| RepresentableList xs => RepresentableList (x ': xs :: [k]) Source # | |
Defined in Numeric.TypedList | |
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