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

Copyright(c) Artem Chirkin
LicenseBSD3
Safe HaskellNone
LanguageHaskell2010

Numeric.Dimensions.Dim

Contents

Description

This module provides KnownDim class that is similar to KnownNat from TypeNats, but keeps Words instead of Naturals; 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 type-level operations.

Provides a data type Dims ds to keep dimension sizes for multiple-dimensional data. 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.

Synopsis

Dim -- a Nat-indexed dimension

Type level numbers that can be unknown.

data XNat Source #

Either known or unknown at compile-time natural number

Constructors

XN Nat 
N Nat 
Instances
KnownDimKind XNat Source # 
Instance details

Defined in Numeric.Dimensions.Dim

BoundedDims ([] :: [XNat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound [] :: [Nat] Source #

KnownDim m => BoundedDim (XN m :: XNat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound (XN m) :: Nat Source #

Methods

dimBound :: Dim (DimBound (XN m)) Source #

constrainDim :: Dim y -> Maybe (Dim (XN m)) Source #

KnownDim n => BoundedDim (N n :: XNat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound (N n) :: Nat Source #

Methods

dimBound :: Dim (DimBound (N n)) Source #

constrainDim :: Dim y -> Maybe (Dim (N n)) Source #

(BoundedDim n, BoundedDims ns) => BoundedDims (n ': ns :: [XNat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound (n ': ns) :: [Nat] Source #

Methods

dimsBound :: Dims (DimsBound (n ': ns)) Source #

constrainDims :: Dims ys -> Maybe (Dims (n ': ns)) Source #

inferAllBoundedDims :: Dict (All BoundedDim (n ': ns), RepresentableList (n ': ns)) Source #

Eq (Dim x) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dim x -> Dim x -> Bool #

(/=) :: Dim x -> Dim x -> Bool #

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool #

(/=) :: Dims ds -> Dims ds -> Bool #

Ord (Dim x) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dim x -> Dim x -> Ordering #

(<) :: Dim x -> Dim x -> Bool #

(<=) :: Dim x -> Dim x -> Bool #

(>) :: Dim x -> Dim x -> Bool #

(>=) :: Dim x -> Dim x -> Bool #

max :: Dim x -> Dim x -> Dim x #

min :: Dim x -> Dim x -> Dim x #

Ord (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dims ds -> Dims ds -> Ordering #

(<) :: Dims ds -> Dims ds -> Bool #

(<=) :: Dims ds -> Dims ds -> Bool #

(>) :: Dims ds -> Dims ds -> Bool #

(>=) :: Dims ds -> Dims ds -> Bool #

max :: Dims ds -> Dims ds -> Dims ds #

min :: Dims ds -> Dims ds -> Dims ds #

type DimsBound ([] :: [XNat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimsBound ([] :: [XNat]) = ([] :: [Nat])
type DimBound (XN m :: XNat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimBound (XN m :: XNat) = m
type DimBound (N n :: XNat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimBound (N n :: XNat) = n
type DimsBound (n ': ns :: [XNat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimsBound (n ': ns :: [XNat]) = DimBound n ': DimsBound ns

type XN (n :: Nat) = XN n Source #

Unknown natural number, known to be not smaller than the given Nat

type N (n :: Nat) = N n Source #

Known natural number

data XNatType :: XNat -> Type where Source #

Find out whether XNat is of known or constrained type.

Constructors

Nt :: XNatType (N n)

Given XNat is known

XNt :: XNatType (XN m)

Given XNat is constrained unknown

Term level dimension

data Dim (x :: k) where Source #

Singleton type to store type-level dimension value.

On the one hand, it can be used to let type-inference system know relations between type-level 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 XNats to represent them.

Bundled Patterns

pattern D :: forall (n :: Nat). () => KnownDim n => Dim n

Match against this pattern to bring KnownDim instance into scope.

pattern Dn :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat). (KnownDim n, xn ~ N n) => Dim n -> Dim xn

Statically known XNat

pattern Dx :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat) (m :: Nat). (KnownDim n, m <= n, xn ~ XN m) => Dim n -> Dim xn

XNat that is unknown at compile time. Same as SomeNat, but for a dimension: Hide dimension size inside, but allow specifying its minimum possible value.

pattern D0 :: forall (n :: Nat). () => n ~ 0 => Dim n

Match Dim n against a concrete Nat

pattern D1 :: forall (n :: Nat). () => n ~ 1 => Dim n

Match Dim n against a concrete Nat

pattern D2 :: forall (n :: Nat). () => n ~ 2 => Dim n

Match Dim n against a concrete Nat

pattern D3 :: forall (n :: Nat). () => n ~ 3 => Dim n

Match Dim n against a concrete Nat

pattern D4 :: forall (n :: Nat). () => n ~ 4 => Dim n

Match Dim n against a concrete Nat

pattern D5 :: forall (n :: Nat). () => n ~ 5 => Dim n

Match Dim n against a concrete Nat

pattern D6 :: forall (n :: Nat). () => n ~ 6 => Dim n

Match Dim n against a concrete Nat

pattern D7 :: forall (n :: Nat). () => n ~ 7 => Dim n

Match Dim n against a concrete Nat

pattern D8 :: forall (n :: Nat). () => n ~ 8 => Dim n

Match Dim n against a concrete Nat

pattern D9 :: forall (n :: Nat). () => n ~ 9 => Dim n

Match Dim n against a concrete Nat

pattern D10 :: forall (n :: Nat). () => n ~ 10 => Dim n

Match Dim n against a concrete Nat

pattern D11 :: forall (n :: Nat). () => n ~ 11 => Dim n

Match Dim n against a concrete Nat

pattern D12 :: forall (n :: Nat). () => n ~ 12 => Dim n

Match Dim n against a concrete Nat

pattern D13 :: forall (n :: Nat). () => n ~ 13 => Dim n

Match Dim n against a concrete Nat

pattern D14 :: forall (n :: Nat). () => n ~ 14 => Dim n

Match Dim n against a concrete Nat

pattern D15 :: forall (n :: Nat). () => n ~ 15 => Dim n

Match Dim n against a concrete Nat

pattern D16 :: forall (n :: Nat). () => n ~ 16 => Dim n

Match Dim n against a concrete Nat

pattern D17 :: forall (n :: Nat). () => n ~ 17 => Dim n

Match Dim n against a concrete Nat

pattern D18 :: forall (n :: Nat). () => n ~ 18 => Dim n

Match Dim n against a concrete Nat

pattern D19 :: forall (n :: Nat). () => n ~ 19 => Dim n

Match Dim n against a concrete Nat

pattern D20 :: forall (n :: Nat). () => n ~ 20 => Dim n

Match Dim n against a concrete Nat

pattern D21 :: forall (n :: Nat). () => n ~ 21 => Dim n

Match Dim n against a concrete Nat

pattern D22 :: forall (n :: Nat). () => n ~ 22 => Dim n

Match Dim n against a concrete Nat

pattern D23 :: forall (n :: Nat). () => n ~ 23 => Dim n

Match Dim n against a concrete Nat

pattern D24 :: forall (n :: Nat). () => n ~ 24 => Dim n

Match Dim n against a concrete Nat

pattern D25 :: forall (n :: Nat). () => n ~ 25 => Dim n

Match Dim n against a concrete Nat

Instances
Eq (Dim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dim n -> Dim n -> Bool #

(/=) :: Dim n -> Dim n -> Bool #

Eq (Dim x) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dim x -> Dim x -> Bool #

(/=) :: Dim x -> Dim x -> Bool #

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool #

(/=) :: Dims ds -> Dims ds -> Bool #

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool #

(/=) :: Dims ds -> Dims ds -> Bool #

Typeable d => Data (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

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) #

toConstr :: Dim d -> Constr #

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 # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dim n -> Dim n -> Ordering #

(<) :: Dim n -> Dim n -> Bool #

(<=) :: Dim n -> Dim n -> Bool #

(>) :: Dim n -> Dim n -> Bool #

(>=) :: Dim n -> Dim n -> Bool #

max :: Dim n -> Dim n -> Dim n #

min :: Dim n -> Dim n -> Dim n #

Ord (Dim x) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dim x -> Dim x -> Ordering #

(<) :: Dim x -> Dim x -> Bool #

(<=) :: Dim x -> Dim x -> Bool #

(>) :: Dim x -> Dim x -> Bool #

(>=) :: Dim x -> Dim x -> Bool #

max :: Dim x -> Dim x -> Dim x #

min :: Dim x -> Dim x -> Dim x #

Ord (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dims ds -> Dims ds -> Ordering #

(<) :: Dims ds -> Dims ds -> Bool #

(<=) :: Dims ds -> Dims ds -> Bool #

(>) :: Dims ds -> Dims ds -> Bool #

(>=) :: Dims ds -> Dims ds -> Bool #

max :: Dims ds -> Dims ds -> Dims ds #

min :: Dims ds -> Dims ds -> Dims ds #

Ord (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dims ds -> Dims ds -> Ordering #

(<) :: Dims ds -> Dims ds -> Bool #

(<=) :: Dims ds -> Dims ds -> Bool #

(>) :: Dims ds -> Dims ds -> Bool #

(>=) :: Dims ds -> Dims ds -> Bool #

max :: Dims ds -> Dims ds -> Dims ds #

min :: Dims ds -> Dims ds -> Dims ds #

BoundedDim x => Read (Dim x) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

BoundedDims xs => Read (Dims xs) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Show (Dim x) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

showsPrec :: Int -> Dim x -> ShowS #

show :: Dim x -> String #

showList :: [Dim x] -> ShowS #

Show (Dims xs) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

showsPrec :: Int -> Dims xs -> ShowS #

show :: Dims xs -> String #

showList :: [Dims xs] -> ShowS #

KnownDim d => Generic (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type Rep (Dim d) :: Type -> Type #

Methods

from :: Dim d -> Rep (Dim d) x #

to :: Rep (Dim d) x -> Dim d #

type Rep (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type Rep (Dim d) = D1 (MetaData "Dim" "Numeric.Dim" "dimensions" False) (C1 (MetaCons (AppendSymbol "D" (ShowNat d)) PrefixI False) (U1 :: Type -> Type))

type SomeDim = Dim (XN 0) Source #

Same as SomeNat

class KnownDim (n :: Nat) where Source #

This class provides the Dim associated with a type-level natural.

Note, kind of the KnownDim argument is always Nat, because it is impossible to create a unique KnownDim (XN m) instance.

Methods

dim :: Dim n Source #

Get value of type-level 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
KnownNat n => KnownDim n Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim n Source #

KnownDim 0 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 0 Source #

KnownDim 1 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 1 Source #

KnownDim 2 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 2 Source #

KnownDim 3 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 3 Source #

KnownDim 4 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 4 Source #

KnownDim 5 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 5 Source #

KnownDim 6 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 6 Source #

KnownDim 7 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 7 Source #

KnownDim 8 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 8 Source #

KnownDim 9 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 9 Source #

KnownDim 10 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 10 Source #

KnownDim 11 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 11 Source #

KnownDim 12 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 12 Source #

KnownDim 13 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 13 Source #

KnownDim 14 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 14 Source #

KnownDim 15 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 15 Source #

KnownDim 16 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 16 Source #

KnownDim 17 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 17 Source #

KnownDim 18 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 18 Source #

KnownDim 19 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 19 Source #

KnownDim 20 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 20 Source #

KnownDim 21 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 21 Source #

KnownDim 22 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 22 Source #

KnownDim 23 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 23 Source #

KnownDim 24 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 24 Source #

KnownDim 25 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 25 Source #

Class (KnownNat n) (KnownDim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

cls :: KnownDim n :- KnownNat n #

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.

Associated Types

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).

Methods

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.

Instances
KnownDim n => BoundedDim (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound n :: Nat Source #

KnownDim m => BoundedDim (XN m :: XNat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound (XN m) :: Nat Source #

Methods

dimBound :: Dim (DimBound (XN m)) Source #

constrainDim :: Dim y -> Maybe (Dim (XN m)) Source #

KnownDim n => BoundedDim (N n :: XNat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound (N n) :: Nat Source #

Methods

dimBound :: Dim (DimBound (N n)) Source #

constrainDim :: Dim y -> Maybe (Dim (N n)) Source #

minDim :: forall (k :: Type) (d :: k). BoundedDim d => Dim d Source #

class KnownXNatType (n :: XNat) where Source #

Find out the type of XNat constructor

Methods

xNatType :: XNatType n Source #

Pattern-match against this to out the type of XNat constructor

Instances
KnownXNatType (XN n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

xNatType :: XNatType (XN n) Source #

KnownXNatType (N n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

xNatType :: XNatType (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.

Equations

FixedDim (N a) b = a ~ b 
FixedDim (XN m) b = m <= b 

dimVal :: forall (k :: Type) (x :: k). Dim (x :: k) -> Word Source #

Similar to natVal from TypeNats, but returns Word.

dimVal' :: forall (n :: Nat). KnownDim n => Word Source #

Similar to natVal from TypeNats, but returns Word.

typeableDim :: forall (n :: Nat). Typeable n => Dim n Source #

Construct a Dim n if there is an instance of Typeable n around.

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 type-level 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 type-level numbers, or Nothing.

compareDim :: forall (a :: Nat) (b :: Nat). Dim a -> Dim b -> SOrdering (CmpNat a b) Source #

Ordering of dimension values.

Note: CmpNat forces type parameters to kind Nat; if you want to compare unknown XNats, use Ord instance of Dim.

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 #

Ordering of dimension values.

Note: CmpNat forces type parameters to kind Nat; if you want to compare unknown XNats, use Ord instance of Dim.

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 explicitly-passed 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

plusDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (n + m) Source #

minusDim :: forall (n :: Nat) (m :: Nat). (<=) m n => Dim n -> Dim m -> Dim (n - m) Source #

minusDimM :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Maybe (Dim (n - m)) Source #

timesDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (* n m) Source #

powerDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim ((^) n m) Source #

divDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Div n m) Source #

modDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Mod n m) Source #

log2Dim :: forall (n :: Nat). Dim n -> Dim (Log2 n) Source #

Re-export part of Lits for convenience

data Nat #

(Kind) This is the kind of type-level natural numbers.

Instances
KnownDimKind Nat Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Dimensions ns => BoundedDims (ns :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound ns :: [Nat] Source #

KnownDim n => BoundedDim (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound n :: Nat Source #

Dimensions ([] :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims [] Source #

Dimensions ds => Enum (Idxs ds) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

succ :: Idxs ds -> Idxs ds #

pred :: Idxs ds -> Idxs ds #

toEnum :: Int -> Idxs ds #

fromEnum :: Idxs ds -> Int #

enumFrom :: Idxs ds -> [Idxs ds] #

enumFromThen :: Idxs ds -> Idxs ds -> [Idxs ds] #

enumFromTo :: Idxs ds -> Idxs ds -> [Idxs ds] #

enumFromThenTo :: Idxs ds -> Idxs ds -> Idxs ds -> [Idxs ds] #

Eq (Dim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dim n -> Dim n -> Bool #

(/=) :: Dim n -> Dim n -> Bool #

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool #

(/=) :: Dims ds -> Dims ds -> Bool #

Typeable d => Data (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

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) #

toConstr :: Dim d -> Constr #

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 # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dim n -> Dim n -> Ordering #

(<) :: Dim n -> Dim n -> Bool #

(<=) :: Dim n -> Dim n -> Bool #

(>) :: Dim n -> Dim n -> Bool #

(>=) :: Dim n -> Dim n -> Bool #

max :: Dim n -> Dim n -> Dim n #

min :: Dim n -> Dim n -> Dim n #

Ord (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dims ds -> Dims ds -> Ordering #

(<) :: Dims ds -> Dims ds -> Bool #

(<=) :: Dims ds -> Dims ds -> Bool #

(>) :: Dims ds -> Dims ds -> Bool #

(>=) :: Dims ds -> Dims ds -> Bool #

max :: Dims ds -> Dims ds -> Dims ds #

min :: Dims ds -> Dims ds -> Dims ds #

KnownDim d => Generic (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type Rep (Dim d) :: Type -> Type #

Methods

from :: Dim d -> Rep (Dim d) x #

to :: Rep (Dim d) x -> Dim d #

(KnownDim d, Dimensions ds) => Dimensions (d ': ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims (d ': ds) Source #

type DimsBound (ns :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimsBound (ns :: [Nat]) = ns
type DimBound (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimBound (n :: Nat) = n
type Rep (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type Rep (Dim d) = D1 (MetaData "Dim" "Numeric.Dim" "dimensions" False) (C1 (MetaCons (AppendSymbol "D" (ShowNat d)) PrefixI False) (U1 :: Type -> Type))

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

data SOrdering :: Ordering -> Type where Source #

Singleton-style version of Ordering. Pattern-match againts its constructor to witness the result of type-level comparison.

Constructors

SLT :: SOrdering LT 
SEQ :: SOrdering EQ 
SGT :: SOrdering GT 

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #

Multiplication of type-level naturals.

Since: base-4.7.0.0

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

Exponentiation of type-level naturals.

Since: base-4.7.0.0

type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b) Source #

Comparison of type-level naturals, as a constraint.

Inferring kind of type-level dimension

class KnownDimKind (k :: Type) where Source #

Figure out whether the type-level dimension is Nat or XNat. Useful for generalized inference functions.

Methods

dimKind :: DimKind k Source #

Instances
KnownDimKind Nat Source # 
Instance details

Defined in Numeric.Dimensions.Dim

KnownDimKind XNat Source # 
Instance details

Defined in Numeric.Dimensions.Dim

data DimKind :: Type -> Type where Source #

GADT to support KnownDimKind type class. Match against its constructors to know if k is Nat or XNat

Constructors

DimNat :: DimKind Nat

Working on Nat.

DimXNat :: DimKind XNat

Working on XNat.

Dims -- a list of dimensions

type Dims (xs :: [k]) = TypedList Dim xs Source #

Type-level dimensionality.

data SomeDims Source #

Same as SomeNat, but for Dimensions: Hide all information about Dimensions inside

Constructors

SomeDims (Dims ns) 

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).

Methods

dims :: Dims ds Source #

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 # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims [] Source #

(KnownDim d, Dimensions ds) => Dimensions (d ': ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims (d ': ds) Source #

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 implies BoundedDims ds.

Associated Types

type DimsBound ds :: [Nat] Source #

Minimal or exact bound of Dims. This is a plural form of DimBound.

Methods

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 on-demand.

Instances
Dimensions ns => BoundedDims (ns :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound ns :: [Nat] Source #

BoundedDims ([] :: [XNat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound [] :: [Nat] Source #

(BoundedDim n, BoundedDims ns) => BoundedDims (n ': ns :: [XNat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound (n ': ns) :: [Nat] Source #

Methods

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 #

Type-indexed list

Bundled Patterns

pattern Dims :: forall (ds :: [Nat]). () => Dimensions ds => Dims ds

O(1) Pattern-matching against this constructor brings a Dimensions instance into the scope. Thus, you can do arbitrary operations on your dims and use this pattern at any time to reconstruct the class instance at runtime.

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 Dims at runtime; for example, reading a list of dimensions from a file.

In order to use this pattern, one must know XNat type constructors in each dimension at compile time.

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 :: [Nat]). () => (All KnownDim ds, All BoundedDim ds, RepresentableList ds, Dimensions ds) => Dims ds

O(Length ds) A heavy weapon against all sorts of type errors

pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs

Zero-length 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 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 TypeList :: forall (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs

Pattern matching against this causes RepresentableList instance come into scope. Also it allows constructing a term-level list out of a constraint.

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 type-indexed 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 type-indexed 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 # 
Instance details

Defined in Numeric.Tuple.Strict

Methods

minBound :: Tuple xs #

maxBound :: Tuple xs #

(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

Methods

minBound :: Tuple xs #

maxBound :: Tuple xs #

All Eq xs => Eq (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Strict

Methods

(==) :: Tuple xs -> Tuple xs -> Bool #

(/=) :: Tuple xs -> Tuple xs -> Bool #

All Eq xs => Eq (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

Methods

(==) :: Tuple xs -> Tuple xs -> Bool #

(/=) :: Tuple xs -> Tuple xs -> Bool #

(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #

Lexicorgaphic ordering; same as normal Haskell lists.

Instance details

Defined in Numeric.Tuple.Strict

Methods

compare :: Tuple xs -> Tuple xs -> Ordering #

(<) :: Tuple xs -> Tuple xs -> Bool #

(<=) :: Tuple xs -> Tuple xs -> Bool #

(>) :: Tuple xs -> Tuple xs -> Bool #

(>=) :: Tuple xs -> Tuple xs -> Bool #

max :: Tuple xs -> Tuple xs -> Tuple xs #

min :: Tuple xs -> Tuple xs -> Tuple xs #

(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #

Lexicorgaphic ordering; same as normal Haskell lists.

Instance details

Defined in Numeric.Tuple.Lazy

Methods

compare :: Tuple xs -> Tuple xs -> Ordering #

(<) :: Tuple xs -> Tuple xs -> Bool #

(<=) :: Tuple xs -> Tuple xs -> Bool #

(>) :: Tuple xs -> Tuple xs -> Bool #

(>=) :: Tuple xs -> Tuple xs -> Bool #

max :: Tuple xs -> Tuple xs -> Tuple xs #

min :: Tuple xs -> Tuple xs -> Tuple xs #

(All Read xs, RepresentableList xs) => Read (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Strict

(All Read xs, RepresentableList xs) => Read (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

All Show xs => Show (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Strict

Methods

showsPrec :: Int -> Tuple xs -> ShowS #

show :: Tuple xs -> String #

showList :: [Tuple xs] -> ShowS #

All Show xs => Show (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

Methods

showsPrec :: Int -> Tuple xs -> ShowS #

show :: Tuple xs -> String #

showList :: [Tuple xs] -> ShowS #

All Semigroup xs => Semigroup (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Strict

Methods

(<>) :: Tuple xs -> Tuple xs -> Tuple xs #

sconcat :: NonEmpty (Tuple xs) -> Tuple xs #

stimes :: Integral b => b -> Tuple xs -> Tuple xs #

All Semigroup xs => Semigroup (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

Methods

(<>) :: Tuple xs -> Tuple xs -> Tuple xs #

sconcat :: NonEmpty (Tuple xs) -> Tuple xs #

stimes :: Integral b => b -> Tuple xs -> Tuple xs #

(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Strict

Methods

mempty :: Tuple xs #

mappend :: Tuple xs -> Tuple xs -> Tuple xs #

mconcat :: [Tuple xs] -> Tuple xs #

(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

Methods

mempty :: Tuple xs #

mappend :: Tuple xs -> Tuple xs -> Tuple xs #

mconcat :: [Tuple xs] -> Tuple xs #

BoundedDims ds => Bounded (Idxs ds) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

minBound :: Idxs ds #

maxBound :: Idxs ds #

Dimensions ds => Enum (Idxs ds) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

succ :: Idxs ds -> Idxs ds #

pred :: Idxs ds -> Idxs ds #

toEnum :: Int -> Idxs ds #

fromEnum :: Idxs ds -> Int #

enumFrom :: Idxs ds -> [Idxs ds] #

enumFromThen :: Idxs ds -> Idxs ds -> [Idxs ds] #

enumFromTo :: Idxs ds -> Idxs ds -> [Idxs ds] #

enumFromThenTo :: Idxs ds -> Idxs ds -> Idxs ds -> [Idxs ds] #

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool #

(/=) :: Dims ds -> Dims ds -> Bool #

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool #

(/=) :: Dims ds -> Dims ds -> Bool #

Eq (Idxs xs) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

(==) :: Idxs xs -> Idxs xs -> Bool #

(/=) :: Idxs xs -> Idxs xs -> Bool #

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)
Instance details

Defined in Numeric.Dimensions.Idx

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) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dims ds -> Dims ds -> Ordering #

(<) :: Dims ds -> Dims ds -> Bool #

(<=) :: Dims ds -> Dims ds -> Bool #

(>) :: Dims ds -> Dims ds -> Bool #

(>=) :: Dims ds -> Dims ds -> Bool #

max :: Dims ds -> Dims ds -> Dims ds #

min :: Dims ds -> Dims ds -> Dims ds #

Ord (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

compare :: Dims ds -> Dims ds -> Ordering #

(<) :: Dims ds -> Dims ds -> Bool #

(<=) :: Dims ds -> Dims ds -> Bool #

(>) :: Dims ds -> Dims ds -> Bool #

(>=) :: Dims ds -> Dims ds -> Bool #

max :: Dims ds -> Dims ds -> Dims ds #

min :: Dims ds -> Dims ds -> Dims ds #

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 compare rule, as for Dims. This is also consistent with offsets:

sort == sortOn fromEnum
Instance details

Defined in Numeric.Dimensions.Idx

Methods

compare :: Idxs xs -> Idxs xs -> Ordering #

(<) :: Idxs xs -> Idxs xs -> Bool #

(<=) :: Idxs xs -> Idxs xs -> Bool #

(>) :: Idxs xs -> Idxs xs -> Bool #

(>=) :: Idxs xs -> Idxs xs -> Bool #

max :: Idxs xs -> Idxs xs -> Idxs xs #

min :: Idxs xs -> Idxs xs -> Idxs xs #

BoundedDims xs => Read (Dims xs) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

BoundedDims xs => Read (Idxs xs) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Show (Dims xs) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

showsPrec :: Int -> Dims xs -> ShowS #

show :: Dims xs -> String #

showList :: [Dims xs] -> ShowS #

Show (Idxs xs) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

showsPrec :: Int -> Idxs xs -> ShowS #

show :: Idxs xs -> String #

showList :: [Idxs xs] -> ShowS #

(Typeable k, Typeable f, Typeable xs, All Data (Map f xs)) => Data (TypedList f xs) Source #

Term-level structure of a TypedList f xs is fully determined by its type Typeable xs. Thus, gunfold does not use its last argument (Constr) at all, relying on the structure of the type parameter.

Instance details

Defined in Numeric.TypedList

Methods

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 # 
Instance details

Defined in Numeric.TypedList

Associated Types

type Rep (TypedList f xs) :: Type -> Type #

Methods

from :: TypedList f xs -> Rep (TypedList f xs) x #

to :: Rep (TypedList f xs) x -> TypedList f xs #

type Rep (TypedList f xs) Source # 
Instance details

Defined in Numeric.TypedList

type Rep (TypedList f xs)

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 type-level 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 type-level 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 type-level 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 #

Similar to const or asProxyTypeOf; to be used on such implicit functions as dim, dimMax, etc.

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 XNat-indexed dims given their fixed counterpart.

xDims' :: forall (xns :: [XNat]) (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims xns Source #

Get XNat-indexed 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.

Type-level programming

type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where ... Source #

Map Dims onto XDims (injective)

Equations

AsXDims '[] = '[] 
AsXDims (n ': ns) = N n ': AsXDims ns 

type family AsDims (xns :: [XNat]) = (ns :: [Nat]) | ns -> xns where ... Source #

Map XDims onto Dims (injective)

Equations

AsDims '[] = '[] 
AsDims (N x ': xs) = x ': AsDims xs 

type family FixedDims (xns :: [XNat]) (ns :: [Nat]) :: Constraint where ... Source #

Constrain Nat dimensions hidden behind XNats.

Equations

FixedDims '[] ns = ns ~ '[] 
FixedDims (xn ': xns) ns = (ns ~ (Head ns ': Tail ns), FixedDim xn (Head ns), FixedDims xns (Tail ns)) 

type KnownXNatTypes xns = All KnownXNatType xns Source #

Know the structure of each dimension

Re-export type list

class RepresentableList (xs :: [k]) where Source #

Representable type lists. Allows getting type information about list structure at runtime.

Methods

tList :: TypeList xs Source #

Get type-level constructed list

Instances
RepresentableList ([] :: [k]) Source # 
Instance details

Defined in Numeric.TypedList

Methods

tList :: TypeList [] Source #

RepresentableList xs => RepresentableList (x ': xs :: [k]) Source # 
Instance details

Defined in Numeric.TypedList

Methods

tList :: TypeList (x ': xs) Source #

type TypeList (xs :: [k]) = TypedList Proxy xs Source #

A list of type proxies

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 -> ...

order :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs) Source #

order' :: forall (k :: Type) (xs :: [k]). RepresentableList xs => Dim (Length xs) Source #