Copyright  (c) Artem Chirkin 

License  BSD3 
Safe Haskell  None 
Language  Haskell2010 
This module provides KnownDim
class that is similar to KnownNat
from TypeNats
,
but keeps Word
s instead of Natural
s;
Also it provides Dim
data type serving as a singleton
suitable for recovering an instance of the KnownDim
class.
A set of utility functions provide inference functionality, so
that KnownDim
can be preserved over some typelevel operations.
Provides a data type Dims ds
to keep dimension sizes
for multipledimensional data.
Higher indices go first, i.e. assumed enumeration
is i = i1*n1*n2*...*n(k1) + ... + i(k2)*n1*n2 + i(k1)*n1 + ik
This corresponds to rowfirst layout of matrices and multidimenional arrays.
Synopsis
 data XNat
 type XN (n :: Nat) = XN n
 type N (n :: Nat) = N n
 data XNatType :: XNat > Type where
 data Dim (x :: k) where
 pattern D :: forall (n :: Nat). () => KnownDim n => Dim n
 pattern Dn :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat). (KnownDim n, xn ~ N n) => Dim n > Dim xn
 pattern Dx :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat) (m :: Nat). (KnownDim n, m <= n, xn ~ XN m) => Dim n > Dim xn
 pattern D0 :: forall (n :: Nat). () => n ~ 0 => Dim n
 pattern D1 :: forall (n :: Nat). () => n ~ 1 => Dim n
 pattern D2 :: forall (n :: Nat). () => n ~ 2 => Dim n
 pattern D3 :: forall (n :: Nat). () => n ~ 3 => Dim n
 pattern D4 :: forall (n :: Nat). () => n ~ 4 => Dim n
 pattern D5 :: forall (n :: Nat). () => n ~ 5 => Dim n
 pattern D6 :: forall (n :: Nat). () => n ~ 6 => Dim n
 pattern D7 :: forall (n :: Nat). () => n ~ 7 => Dim n
 pattern D8 :: forall (n :: Nat). () => n ~ 8 => Dim n
 pattern D9 :: forall (n :: Nat). () => n ~ 9 => Dim n
 pattern D10 :: forall (n :: Nat). () => n ~ 10 => Dim n
 pattern D11 :: forall (n :: Nat). () => n ~ 11 => Dim n
 pattern D12 :: forall (n :: Nat). () => n ~ 12 => Dim n
 pattern D13 :: forall (n :: Nat). () => n ~ 13 => Dim n
 pattern D14 :: forall (n :: Nat). () => n ~ 14 => Dim n
 pattern D15 :: forall (n :: Nat). () => n ~ 15 => Dim n
 pattern D16 :: forall (n :: Nat). () => n ~ 16 => Dim n
 pattern D17 :: forall (n :: Nat). () => n ~ 17 => Dim n
 pattern D18 :: forall (n :: Nat). () => n ~ 18 => Dim n
 pattern D19 :: forall (n :: Nat). () => n ~ 19 => Dim n
 pattern D20 :: forall (n :: Nat). () => n ~ 20 => Dim n
 pattern D21 :: forall (n :: Nat). () => n ~ 21 => Dim n
 pattern D22 :: forall (n :: Nat). () => n ~ 22 => Dim n
 pattern D23 :: forall (n :: Nat). () => n ~ 23 => Dim n
 pattern D24 :: forall (n :: Nat). () => n ~ 24 => Dim n
 pattern D25 :: forall (n :: Nat). () => n ~ 25 => Dim n
 type SomeDim = Dim (XN 0)
 class KnownDim (n :: Nat) where
 class KnownDimKind k => BoundedDim (n :: k) where
 minDim :: forall (k :: Type) (d :: k). BoundedDim d => Dim d
 class KnownXNatType (n :: XNat) where
 type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where ...
 dimVal :: forall (k :: Type) (x :: k). Dim (x :: k) > Word
 dimVal' :: forall (n :: Nat). KnownDim n => Word
 typeableDim :: forall (n :: Nat). Typeable n => Dim n
 someDimVal :: Word > SomeDim
 sameDim :: forall (x :: Nat) (y :: Nat). Dim x > Dim y > Maybe (Dict (x ~ y))
 sameDim' :: forall (x :: Nat) (y :: Nat) (p :: Nat > Type) (q :: Nat > Type). (KnownDim x, KnownDim y) => p x > q y > Maybe (Dict (x ~ y))
 compareDim :: forall (a :: Nat) (b :: Nat). Dim a > Dim b > SOrdering (CmpNat a b)
 compareDim' :: forall (a :: Nat) (b :: Nat) (p :: Nat > Type) (q :: Nat > Type). (KnownDim a, KnownDim b) => p a > q b > SOrdering (CmpNat a b)
 constrainBy :: forall (k :: Type) (x :: k) (p :: k > Type) (l :: Type) (y :: l). BoundedDim x => p x > Dim y > Maybe (Dim x)
 relax :: forall (m :: Nat) (n :: Nat). (<=) m n => Dim (XN n) > Dim (XN m)
 plusDim :: forall (n :: Nat) (m :: Nat). Dim n > Dim m > Dim (n + m)
 minusDim :: forall (n :: Nat) (m :: Nat). (<=) m n => Dim n > Dim m > Dim (n  m)
 minusDimM :: forall (n :: Nat) (m :: Nat). Dim n > Dim m > Maybe (Dim (n  m))
 timesDim :: forall (n :: Nat) (m :: Nat). Dim n > Dim m > Dim (* n m)
 powerDim :: forall (n :: Nat) (m :: Nat). Dim n > Dim m > Dim ((^) n m)
 divDim :: forall (n :: Nat) (m :: Nat). Dim n > Dim m > Dim (Div n m)
 modDim :: forall (n :: Nat) (m :: Nat). Dim n > Dim m > Dim (Mod n m)
 log2Dim :: forall (n :: Nat). Dim n > Dim (Log2 n)
 data Nat
 type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
 data SOrdering :: Ordering > Type where
 type family (a :: Nat) + (b :: Nat) :: Nat where ...
 type family (a :: Nat)  (b :: Nat) :: Nat where ...
 type family (a :: Nat) * (b :: Nat) :: Nat where ...
 type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
 type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b)
 class KnownDimKind (k :: Type) where
 data DimKind :: Type > Type where
 type Dims (xs :: [k]) = TypedList Dim xs
 data SomeDims = SomeDims (Dims ns)
 class Dimensions (ds :: [Nat]) where
 class KnownDimKind k => BoundedDims (ds :: [k]) where
 type DimsBound ds :: [Nat]
 dimsBound :: Dims (DimsBound ds)
 constrainDims :: forall (l :: Type) (ys :: [l]). Dims ys > Maybe (Dims ds)
 inferAllBoundedDims :: Dict (All BoundedDim ds, RepresentableList ds)
 minDims :: forall (k :: Type) (ds :: [k]). BoundedDims ds => Dims ds
 data TypedList (f :: k > Type) (xs :: [k]) where
 pattern Dims :: forall (ds :: [Nat]). () => 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 :: [Nat]). () => (All KnownDim ds, All BoundedDim ds, RepresentableList ds, Dimensions ds) => Dims ds
 pattern U :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
 pattern (:*) :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y > TypedList f ys > TypedList f xs
 pattern Empty :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
 pattern TypeList :: forall (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs
 pattern Cons :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y > TypedList f ys > TypedList f xs
 pattern Snoc :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy > f y > TypedList f xs
 pattern Reverse :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => TypedList f sx > TypedList f xs
 typeableDims :: forall (ds :: [Nat]). Typeable ds => Dims ds
 inferTypeableDims :: forall (ds :: [Nat]). Dims ds > Dict (Typeable ds)
 listDims :: forall (k :: Type) (xs :: [k]). Dims xs > [Word]
 someDimsVal :: [Word] > SomeDims
 totalDim :: forall (k :: Type) (xs :: [k]). Dims xs > Word
 totalDim' :: forall (xs :: [Nat]). Dimensions xs => Word
 sameDims :: forall (as :: [Nat]) (bs :: [Nat]). Dims as > Dims bs > Maybe (Dict (as ~ bs))
 sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) (p :: [Nat] > Type) (q :: [Nat] > Type). (Dimensions as, Dimensions bs) => p as > q bs > Maybe (Dict (as ~ bs))
 inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] > Type) (q :: [k] > Type). p ds > q ds > p ds
 asSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] > Type) (q :: [k] > Type) (r :: Type). p ds > (q ds > r) > q ds > r
 xDims :: forall (xns :: [XNat]) (ns :: [Nat]). FixedDims xns ns => Dims ns > Dims xns
 xDims' :: forall (xns :: [XNat]) (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims xns
 stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat]). Dims xs > Dims ys > Maybe (Dims (StripPrefix xs ys))
 stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat]). Dims xs > Dims ys > Maybe (Dims (StripSuffix xs ys))
 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
 class RepresentableList (xs :: [k]) where
 type TypeList (xs :: [k]) = TypedList Proxy xs
 types :: forall (k :: Type) (f :: k > Type) (xs :: [k]). TypedList f xs > TypeList xs
 order :: forall (k :: Type) (f :: k > Type) (xs :: [k]). TypedList f xs > Dim (Length xs)
 order' :: forall (k :: Type) (xs :: [k]). RepresentableList xs => Dim (Length xs)
Dim
 a Nat
indexed dimension
Type level numbers that can be unknown.
Either known or unknown at compiletime natural number
Instances
type XN (n :: Nat) = XN n Source #
Unknown natural number, known to be not smaller than the given Nat
Term level dimension
data Dim (x :: k) where Source #
Singleton type to store typelevel dimension value.
On the one hand, it can be used to let typeinference system know
relations between typelevel naturals.
On the other hand, this is just a newtype wrapper on the Word
type.
Usually, the type parameter of Dim
is either Nat
or XNat
.
If dimensionality of your data is known in advance, use Nat
;
if you know the size of some dimensions, but do not know the size
of others, use XNat
s to represent them.
pattern D :: forall (n :: Nat). () => KnownDim n => Dim n  Match against this pattern to bring 
pattern Dn :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat). (KnownDim n, xn ~ N n) => Dim n > Dim xn  Statically known 
pattern Dx :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat) (m :: Nat). (KnownDim n, m <= n, xn ~ XN m) => Dim n > Dim xn 

pattern D0 :: forall (n :: Nat). () => n ~ 0 => Dim n  Match 
pattern D1 :: forall (n :: Nat). () => n ~ 1 => Dim n  Match 
pattern D2 :: forall (n :: Nat). () => n ~ 2 => Dim n  Match 
pattern D3 :: forall (n :: Nat). () => n ~ 3 => Dim n  Match 
pattern D4 :: forall (n :: Nat). () => n ~ 4 => Dim n  Match 
pattern D5 :: forall (n :: Nat). () => n ~ 5 => Dim n  Match 
pattern D6 :: forall (n :: Nat). () => n ~ 6 => Dim n  Match 
pattern D7 :: forall (n :: Nat). () => n ~ 7 => Dim n  Match 
pattern D8 :: forall (n :: Nat). () => n ~ 8 => Dim n  Match 
pattern D9 :: forall (n :: Nat). () => n ~ 9 => Dim n  Match 
pattern D10 :: forall (n :: Nat). () => n ~ 10 => Dim n  Match 
pattern D11 :: forall (n :: Nat). () => n ~ 11 => Dim n  Match 
pattern D12 :: forall (n :: Nat). () => n ~ 12 => Dim n  Match 
pattern D13 :: forall (n :: Nat). () => n ~ 13 => Dim n  Match 
pattern D14 :: forall (n :: Nat). () => n ~ 14 => Dim n  Match 
pattern D15 :: forall (n :: Nat). () => n ~ 15 => Dim n  Match 
pattern D16 :: forall (n :: Nat). () => n ~ 16 => Dim n  Match 
pattern D17 :: forall (n :: Nat). () => n ~ 17 => Dim n  Match 
pattern D18 :: forall (n :: Nat). () => n ~ 18 => Dim n  Match 
pattern D19 :: forall (n :: Nat). () => n ~ 19 => Dim n  Match 
pattern D20 :: forall (n :: Nat). () => n ~ 20 => Dim n  Match 
pattern D21 :: forall (n :: Nat). () => n ~ 21 => Dim n  Match 
pattern D22 :: forall (n :: Nat). () => n ~ 22 => Dim n  Match 
pattern D23 :: forall (n :: Nat). () => n ~ 23 => Dim n  Match 
pattern D24 :: forall (n :: Nat). () => n ~ 24 => Dim n  Match 
pattern D25 :: forall (n :: Nat). () => n ~ 25 => Dim n  Match 
Instances
Eq (Dim n) Source #  
Eq (Dim x) Source #  
Eq (Dims ds) Source #  
Eq (Dims ds) Source #  
Typeable d => Data (Dim d) Source #  
Defined in Numeric.Dimensions.Dim gfoldl :: (forall d0 b. Data d0 => c (d0 > b) > d0 > c b) > (forall g. g > c g) > Dim d > c (Dim d) # gunfold :: (forall b r. Data b => c (b > r) > c r) > (forall r. r > c r) > Constr > c (Dim d) # dataTypeOf :: Dim d > DataType # dataCast1 :: Typeable t => (forall d0. Data d0 => c (t d0)) > Maybe (c (Dim d)) # dataCast2 :: Typeable t => (forall d0 e. (Data d0, Data e) => c (t d0 e)) > Maybe (c (Dim d)) # gmapT :: (forall b. Data b => b > b) > Dim d > Dim d # gmapQl :: (r > r' > r) > r > (forall d0. Data d0 => d0 > r') > Dim d > r # gmapQr :: (r' > r > r) > r > (forall d0. Data d0 => d0 > r') > Dim d > r # gmapQ :: (forall d0. Data d0 => d0 > u) > Dim d > [u] # gmapQi :: Int > (forall d0. Data d0 => d0 > u) > Dim d > u # gmapM :: Monad m => (forall d0. Data d0 => d0 > m d0) > Dim d > m (Dim d) # gmapMp :: MonadPlus m => (forall d0. Data d0 => d0 > m d0) > Dim d > m (Dim d) # gmapMo :: MonadPlus m => (forall d0. Data d0 => d0 > m d0) > Dim d > m (Dim d) #  
Ord (Dim n) Source #  
Ord (Dim x) Source #  
Ord (Dims ds) Source #  
Ord (Dims ds) Source #  
BoundedDim x => Read (Dim x) Source #  
BoundedDims xs => Read (Dims xs) Source #  
Show (Dim x) Source #  
Show (Dims xs) Source #  
KnownDim d => Generic (Dim d) Source #  
type Rep (Dim d) Source #  
class KnownDim (n :: Nat) where Source #
This class provides the Dim
associated with a typelevel natural.
Note, kind of the KnownDim
argument is always Nat
, because
it is impossible to create a unique KnownDim (XN m)
instance.
Get value of typelevel dim at runtime.
Note, this function is supposed to be used with TypeApplications
.
For example, you can type:
>>>
:set XTypeApplications
>>>
:set XDataKinds
>>>
:t dim @3
dim @3 :: Dim 3
>>>
:set XTypeOperators
>>>
:t dim @(13  6)
dim @(13  6) :: Dim 7
Instances
class KnownDimKind k => BoundedDim (n :: k) where Source #
Get a minimal or exact bound of a Dim
.
To satisfy the BoundedDim
means to be equal to N n
or be not less than XN m
.
type DimBound n :: Nat Source #
Minimal or exact bound of a Dim
.
Useful for indexing: it is safe to index something by an index less than
DimBound n
(for both Nat
and Xnat
indexed dims).
dimBound :: Dim (DimBound n) Source #
Get such a minimal Dim (DimBound n)
, that Dim n
is guaranteed
to be not less than dimBound
if n ~ XN a
,
otherwise, the return Dim
is the same as n
.
constrainDim :: forall (l :: Type) (y :: l). Dim y > Maybe (Dim n) Source #
If the runtime value of Dim y
satisfies dimBound
k x
,
then coerce to Dim x
. Otherwise, return Nothing
.
To satisfy the dimBound
means to be equal to N n
or be not less than XN m
.
class KnownXNatType (n :: XNat) where Source #
Find out the type of XNat
constructor
Instances
KnownXNatType (XN n) Source #  
KnownXNatType (N n) Source #  
type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where ... Source #
Constraints given by an XNat type on possible values of a Nat hidden inside.
typeableDim :: forall (n :: Nat). Typeable n => Dim n Source #
Construct a Dim n
if there is an instance of Typeable n
around.
someDimVal :: Word > SomeDim Source #
Similar to someNatVal
from TypeNats
.
sameDim :: forall (x :: Nat) (y :: Nat). Dim x > Dim y > Maybe (Dict (x ~ y)) Source #
We either get evidence that this function was instantiated with the same typelevel numbers, or Nothing.
Note, this function works on Nat
indexed dimensions only,
because Dim (XN x)
does not have runtime evidence to infer x
and `KnownDim x` does not imply `KnownDim (XN x)`.
sameDim' :: forall (x :: Nat) (y :: Nat) (p :: Nat > Type) (q :: Nat > Type). (KnownDim x, KnownDim y) => p x > q y > Maybe (Dict (x ~ y)) Source #
We either get evidence that this function was instantiated with the same typelevel numbers, or Nothing.
compareDim' :: forall (a :: Nat) (b :: Nat) (p :: Nat > Type) (q :: Nat > Type). (KnownDim a, KnownDim b) => p a > q b > SOrdering (CmpNat a b) Source #
constrainBy :: forall (k :: Type) (x :: k) (p :: k > Type) (l :: Type) (y :: l). BoundedDim x => p x > Dim y > Maybe (Dim x) Source #
constrainDim
with explicitlypassed constraining Dim
to avoid AllowAmbiguousTypes
.
relax :: forall (m :: Nat) (n :: Nat). (<=) m n => Dim (XN n) > Dim (XN m) Source #
Decrease minimum allowed size of a Dim (XN x)
.
Simple Dim arithmetics
Reexport part of
Lits
for convenience
(Kind) This is the kind of typelevel natural numbers.
Instances
KnownDimKind Nat Source #  
Dimensions ns => BoundedDims (ns :: [Nat]) Source #  
Defined in Numeric.Dimensions.Dim dimsBound :: Dims (DimsBound ns) Source # constrainDims :: Dims ys > Maybe (Dims ns) Source # inferAllBoundedDims :: Dict (All BoundedDim ns, RepresentableList ns) Source #  
KnownDim n => BoundedDim (n :: Nat) Source #  
Dimensions ([] :: [Nat]) Source #  
Defined in Numeric.Dimensions.Dim  
Dimensions ds => Enum (Idxs ds) Source #  
Eq (Dim n) Source #  
Eq (Dims ds) Source #  
Typeable d => Data (Dim d) Source #  
Defined in Numeric.Dimensions.Dim gfoldl :: (forall d0 b. Data d0 => c (d0 > b) > d0 > c b) > (forall g. g > c g) > Dim d > c (Dim d) # gunfold :: (forall b r. Data b => c (b > r) > c r) > (forall r. r > c r) > Constr > c (Dim d) # dataTypeOf :: Dim d > DataType # dataCast1 :: Typeable t => (forall d0. Data d0 => c (t d0)) > Maybe (c (Dim d)) # dataCast2 :: Typeable t => (forall d0 e. (Data d0, Data e) => c (t d0 e)) > Maybe (c (Dim d)) # gmapT :: (forall b. Data b => b > b) > Dim d > Dim d # gmapQl :: (r > r' > r) > r > (forall d0. Data d0 => d0 > r') > Dim d > r # gmapQr :: (r' > r > r) > r > (forall d0. Data d0 => d0 > r') > Dim d > r # gmapQ :: (forall d0. Data d0 => d0 > u) > Dim d > [u] # gmapQi :: Int > (forall d0. Data d0 => d0 > u) > Dim d > u # gmapM :: Monad m => (forall d0. Data d0 => d0 > m d0) > Dim d > m (Dim d) # gmapMp :: MonadPlus m => (forall d0. Data d0 => d0 > m d0) > Dim d > m (Dim d) # gmapMo :: MonadPlus m => (forall d0. Data d0 => d0 > m d0) > Dim d > m (Dim d) #  
Ord (Dim n) Source #  
Ord (Dims ds) Source #  
KnownDim d => Generic (Dim d) Source #  
(KnownDim d, Dimensions ds) => Dimensions (d ': ds) Source #  
Defined in Numeric.Dimensions.Dim  
type DimsBound (ns :: [Nat]) Source #  
Defined in Numeric.Dimensions.Dim  
type DimBound (n :: Nat) Source #  
Defined in Numeric.Dimensions.Dim  
type Rep (Dim d) Source #  
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #
Comparison of typelevel naturals, as a function.
Since: base4.7.0.0
data SOrdering :: Ordering > Type where Source #
Singletonstyle version of Ordering
.
Patternmatch againts its constructor to witness the result of
typelevel comparison.
type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #
Addition of typelevel naturals.
Since: base4.7.0.0
type family (a :: Nat)  (b :: Nat) :: Nat where ... infixl 6 #
Subtraction of typelevel naturals.
Since: base4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #
Multiplication of typelevel naturals.
Since: base4.7.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of typelevel naturals.
Since: base4.7.0.0
type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b) Source #
Comparison of typelevel naturals, as a constraint.
Inferring kind of typelevel dimension
class KnownDimKind (k :: Type) where Source #
Figure out whether the typelevel dimension is Nat
or XNat
.
Useful for generalized inference functions.
Instances
KnownDimKind Nat Source #  
KnownDimKind XNat Source #  
data DimKind :: Type > Type where Source #
GADT to support KnownDimKind
type class.
Match against its constructors to know if k
is Nat
or XNat
Dims
 a list of dimensions
Same as SomeNat, but for Dimensions: Hide all information about Dimensions inside
class Dimensions (ds :: [Nat]) where Source #
Put runtime evidence of Dims
value inside function constraints.
Similar to KnownDim
or KnownNat
, but for lists of numbers.
Note, kind of the Dimensions
list is always Nat
, restricted by
KnownDim
being also Nat
indexed
(it is impossible to create a unique KnownDim (XN m)
instance).
Get dimensionality of a space at runtime,
represented as a list of Dim
.
Note, this function is supposed to be used with TypeApplications
.
For example, you can type:
>>>
:set XTypeApplications
>>>
:set XDataKinds
>>>
:t dims @'[17, 12]
dims @'[17, 12] :: Dims '[17, 12]
>>>
:t dims @'[]
dims @'[] :: Dims '[]
>>>
:t dims @(Tail '[3,2,5,7])
dims @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7]
Instances
Dimensions ([] :: [Nat]) Source #  
Defined in Numeric.Dimensions.Dim  
(KnownDim d, Dimensions ds) => Dimensions (d ': ds) Source #  
Defined in Numeric.Dimensions.Dim 
class KnownDimKind k => BoundedDims (ds :: [k]) where Source #
Get a minimal or exact bound of Dims
.
This is a plural form of BoundedDim
.
BoundedDims
is a somewhat weaker form of Dimensions
:
 It is defined for both
[Nat]
and[XNat]
;  Instance of
Dimensions ds
always impliesBoundedDims ds
.
type DimsBound ds :: [Nat] Source #
Minimal or exact bound of Dims
.
This is a plural form of DimBound
.
dimsBound :: Dims (DimsBound ds) Source #
Plural form for dimBound
constrainDims :: forall (l :: Type) (ys :: [l]). Dims ys > Maybe (Dims ds) Source #
Plural form for constrainDim
.
Given a Dims ys
, test if its runtime value satisfies constraints imposed by
BoundedDims ds
, and returns it back coerced to Dims ds
on success.
This function allows to guess safely individual dimension values,
as well as the length of the dimension list.
It returns Nothing
if ds
and xds
have different length or if any
of the values in ys
are less than the corresponding values of ds
.
inferAllBoundedDims :: Dict (All BoundedDim ds, RepresentableList ds) Source #
BoundedDims means every element dim is BoundedDim
and also
the length of a dim list is known.
Enforcing this as a superclass would complicate instance relations, so it is better to provide these dictionaries ondemand.
Instances
Dimensions ns => BoundedDims (ns :: [Nat]) Source #  
Defined in Numeric.Dimensions.Dim dimsBound :: Dims (DimsBound ns) Source # constrainDims :: Dims ys > Maybe (Dims ns) Source # inferAllBoundedDims :: Dict (All BoundedDim ns, RepresentableList ns) Source #  
BoundedDims ([] :: [XNat]) Source #  
Defined in Numeric.Dimensions.Dim dimsBound :: Dims (DimsBound []) Source # constrainDims :: Dims ys > Maybe (Dims []) Source # inferAllBoundedDims :: Dict (All BoundedDim [], RepresentableList []) Source #  
(BoundedDim n, BoundedDims ns) => BoundedDims (n ': ns :: [XNat]) Source #  
Defined in Numeric.Dimensions.Dim dimsBound :: Dims (DimsBound (n ': ns)) Source # constrainDims :: Dims ys > Maybe (Dims (n ': ns)) Source # inferAllBoundedDims :: Dict (All BoundedDim (n ': ns), RepresentableList (n ': ns)) Source # 
minDims :: forall (k :: Type) (ds :: [k]). BoundedDims ds => Dims ds Source #
Minimal runtime Dims ds
value that satifies the constraints imposed by
the type signature of Dims ds
.
data TypedList (f :: k > Type) (xs :: [k]) where Source #
Typeindexed list
pattern Dims :: forall (ds :: [Nat]). () => 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 :: [Nat]). () => (All KnownDim ds, All BoundedDim ds, RepresentableList ds, Dimensions ds) => Dims ds 

pattern U :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs  Zerolength type list 
pattern (:*) :: forall (k :: Type) (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 (k :: Type) (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs  Zerolength type list; synonym to 
pattern TypeList :: forall (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs  Pattern matching against this causes 
pattern Cons :: forall (k :: Type) (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 (k :: Type) (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 (k :: Type) (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) Source #  
(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) Source #  
All Eq xs => Eq (Tuple xs) Source #  
All Eq xs => Eq (Tuple xs) Source #  
(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #  Lexicorgaphic ordering; same as normal Haskell lists. 
Defined in Numeric.Tuple.Strict  
(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #  Lexicorgaphic ordering; same as normal Haskell lists. 
Defined in Numeric.Tuple.Lazy  
(All Read xs, RepresentableList xs) => Read (Tuple xs) Source #  
(All Read xs, RepresentableList xs) => Read (Tuple xs) Source #  
All Show xs => Show (Tuple xs) Source #  
All Show xs => Show (Tuple xs) Source #  
All Semigroup xs => Semigroup (Tuple xs) Source #  
All Semigroup xs => Semigroup (Tuple xs) Source #  
(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source #  
(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source #  
BoundedDims ds => Bounded (Idxs ds) Source #  
Dimensions ds => Enum (Idxs ds) Source #  
Eq (Dims ds) Source #  
Eq (Dims ds) Source #  
Eq (Idxs xs) Source #  
BoundedDim n => Num (Idxs (n ': ([] :: [k]))) Source #  With this instance we can slightly reduce indexing expressions, e.g. x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U) 
Defined in Numeric.Dimensions.Idx (+) :: 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) Source #  
Ord (Dims ds) Source #  
Ord (Idxs xs) Source #  Compare indices by their importance in lexicorgaphic order from the first dimension to the last dimension (the first dimension is the most significant one). Literally, compare a b = compare (listIdxs a) (listIdxs b) This is the same sort == sortOn fromEnum 
BoundedDims xs => Read (Dims xs) Source #  
BoundedDims xs => Read (Idxs xs) Source #  
Show (Dims xs) Source #  
Show (Idxs xs) Source #  
(Typeable k, Typeable f, Typeable xs, All Data (Map f xs)) => Data (TypedList f xs) Source #  Termlevel structure of a 
Defined in Numeric.TypedList gfoldl :: (forall d b. Data d => c (d > b) > d > c b) > (forall g. g > c g) > TypedList f xs > c (TypedList f xs) # gunfold :: (forall b r. Data b => c (b > r) > c r) > (forall r. r > c r) > Constr > c (TypedList f xs) # toConstr :: TypedList f xs > Constr # dataTypeOf :: TypedList f xs > DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) > Maybe (c (TypedList f xs)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) > Maybe (c (TypedList f xs)) # gmapT :: (forall b. Data b => b > b) > TypedList f xs > TypedList f xs # gmapQl :: (r > r' > r) > r > (forall d. Data d => d > r') > TypedList f xs > r # gmapQr :: (r' > r > r) > r > (forall d. Data d => d > r') > TypedList f xs > r # gmapQ :: (forall d. Data d => d > u) > TypedList f xs > [u] # gmapQi :: Int > (forall d. Data d => d > u) > TypedList f xs > u # gmapM :: Monad m => (forall d. Data d => d > m d) > TypedList f xs > m (TypedList f xs) # gmapMp :: MonadPlus m => (forall d. Data d => d > m d) > TypedList f xs > m (TypedList f xs) # gmapMo :: MonadPlus m => (forall d. Data d => d > m d) > TypedList f xs > m (TypedList f xs) #  
Generic (TypedList f xs) Source #  
type Rep (TypedList f xs) Source #  
Defined in Numeric.TypedList 
typeableDims :: forall (ds :: [Nat]). Typeable ds => Dims ds Source #
Construct a Dims ds
if there is an instance of Typeable ds
around.
inferTypeableDims :: forall (ds :: [Nat]). Dims ds > Dict (Typeable ds) Source #
Dims (ds :: [Nat])
is always Typeable
.
listDims :: forall (k :: Type) (xs :: [k]). Dims xs > [Word] Source #
Convert `Dims xs` to a plain haskell list of dimension sizes O(1)
.
Note, for XNat
indexed list it returns actual content dimensions,
not the constraint numbers (XN m
)
someDimsVal :: [Word] > SomeDims Source #
Convert a plain haskell list of dimension sizes into an unknown
typelevel dimensionality O(1)
.
totalDim :: forall (k :: Type) (xs :: [k]). Dims xs > Word Source #
Product of all dimension sizes O(Length xs)
.
totalDim' :: forall (xs :: [Nat]). Dimensions xs => Word Source #
Product of all dimension sizes O(Length xs)
.
sameDims :: forall (as :: [Nat]) (bs :: [Nat]). Dims as > Dims bs > Maybe (Dict (as ~ bs)) Source #
We either get evidence that this function was instantiated with the
same typelevel Dimensions, or Nothing
O(Length xs)
.
sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) (p :: [Nat] > Type) (q :: [Nat] > Type). (Dimensions as, Dimensions bs) => p as > q bs > Maybe (Dict (as ~ bs)) Source #
We either get evidence that this function was instantiated with the
same typelevel Dimensions, or Nothing
O(Length xs)
.
inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] > Type) (q :: [k] > Type). p ds > q ds > p ds Source #
asSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] > Type) (q :: [k] > Type) (r :: Type). p ds > (q ds > r) > q ds > r Source #
Similar to asProxyTypeOf
,
Give a hint to type checker to fix the type of a function argument.
xDims :: forall (xns :: [XNat]) (ns :: [Nat]). FixedDims xns ns => Dims ns > Dims xns Source #
Get XNatindexed dims given their fixed counterpart.
xDims' :: forall (xns :: [XNat]) (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims xns Source #
Get XNatindexed dims given their fixed counterpart.
stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat]). Dims xs > Dims ys > Maybe (Dims (StripPrefix xs ys)) Source #
Drop the given prefix from a Dims list. It returns Nothing if the list did not start with the prefix given, or Just the Dims after the prefix, if it does.
stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat]). Dims xs > Dims ys > Maybe (Dims (StripSuffix xs ys)) Source #
Drop the given suffix from a Dims list. It returns Nothing if the list did not end with the suffix given, or Just the Dims before the suffix, if it does.
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
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 :: forall (k :: Type) (f :: k > Type) (xs :: [k]). 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 > ...