Copyright  (c) Artem Chirkin 

License  BSD3 
Maintainer  chirkin@arch.ethz.ch 
Safe Haskell  None 
Language  Haskell2010 
Provides a data type `Dims ds` to keep dimension sizes for multipledimensional data. Lower indices go first, i.e. assumed enumeration is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k1).
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).
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.
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 #
Typeindexed list
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  Patternmatching against this constructor reveals Natkinded 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 Natindexed dims into XNatindexed dims. 
pattern KnownDims :: forall ds. () => (All KnownDim ds, Dimensions ds) => Dims ds 

pattern U :: forall (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs  Zerolength 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 typeindexed list 
pattern Empty :: forall (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs  Zerolength 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 typeindexed 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 typeindexed 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 infinitedimensional 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 infinitedimensional 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 (+) :: 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) #  
Ord (Dims ds) #  
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 
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
typelevel 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 typelevel 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 typelevel 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 XNatindexed dims given their fixed counterpart.
xDims' :: forall xns ns. (FixedDims xns ns, Dimensions ns) => Dims xns Source #
Get XNatindexed dims given their fixed counterpart.
Typelevel 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 XNat
s.
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.
Reexport type list
class RepresentableList (xs :: [k]) where Source #
Representable type lists. Allows getting type information about list structure at runtime.
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 > ...
Reexport single dimension type and functions
module Numeric.Dim