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

Numeric.Dimensions.Dim

Description

Provides a data type Dim 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

# Dimension data types

data Nat :: * #

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

Instances

 Num (Idx ((:) Nat n ([] Nat))) # With this instance we can slightly reduce indexing expressions e.g. x ! (1 :! 2 :! 4) == x ! (1 :! 2 :! 4 :! Z) Methods(+) :: Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) #(-) :: Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) #(*) :: Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) #negate :: Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) #abs :: Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) #signum :: Idx ((Nat ': n) [Nat]) -> Idx ((Nat ': n) [Nat]) #fromInteger :: Integer -> Idx ((Nat ': n) [Nat]) # Dimensions ([] Nat) Source # Methodsdim :: Dim [Nat] [Nat] Source # Dimensions ds => Bounded (Dim [Nat] ds) # MethodsminBound :: Dim [Nat] ds #maxBound :: Dim [Nat] ds # (KnownDim d, Dimensions ds) => Dimensions ((:) Nat d ds) Source # Methodsdim :: Dim [Nat] ((Nat ': d) ds) Source # type (==) Nat a b type (==) Nat a b = EqNat a b

data XNat Source #

Either known or unknown at compile-time natural number

Instances

 XDimensions ([] XNat) Source # MethodswrapDim :: ([XNat] ~ FixedXDim [XNat] ds) [XNat] => Dim [Nat] ds -> Dim [XNat] [XNat] Source # XDimensions xs => XDimensions ((:) XNat (N n) xs) Source # MethodswrapDim :: ([XNat] ~ FixedXDim ((XNat ': N n) xs) ds) ((XNat ': N n) xs) => Dim [Nat] ds -> Dim [XNat] ((XNat ': N n) xs) Source # XDimensions xs => XDimensions ((:) XNat (XN m) xs) Source # MethodswrapDim :: ([XNat] ~ FixedXDim ((XNat ': XN m) xs) ds) ((XNat ': XN m) xs) => Dim [Nat] ds -> Dim [XNat] ((XNat ': XN m) xs) Source #

type XN n = XN n Source #

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

type N n = N n Source #

Known natural number

data Dim ns where Source #

Type-level dimensionality

Constructors

 D :: Dim '[] Zero-rank dimensionality - scalar (:*) :: forall n ns. NatKind [k] l => !(Dim n) -> !(Dim ns) -> Dim (ConsDim n ns) infixr 5 List-like concatenation of dimensionality. NatKind constraint is needed here to infer that Dn :: forall n. KnownDim n => Dim (n :: Nat) Proxy-like constructor Dx :: forall n m. n <= m => !(Dim m) -> Dim (XN n) Nat known at runtime packed into existential constructor

Instances

 Dimensions ds => Bounded (Dim [Nat] ds) Source # MethodsminBound :: Dim [Nat] ds #maxBound :: Dim [Nat] ds # Eq (Dim k ds) Source # Methods(==) :: Dim k ds -> Dim k ds -> Bool #(/=) :: Dim k ds -> Dim k ds -> Bool # Ord (Dim k ds) Source # Methodscompare :: Dim k ds -> Dim k ds -> Ordering #(<) :: Dim k ds -> Dim k ds -> Bool #(<=) :: Dim k ds -> Dim k ds -> Bool #(>) :: Dim k ds -> Dim k ds -> Bool #(>=) :: Dim k ds -> Dim k ds -> Bool #max :: Dim k ds -> Dim k ds -> Dim k ds #min :: Dim k ds -> Dim k ds -> Dim k ds # Show (Dim k ds) Source # MethodsshowsPrec :: Int -> Dim k ds -> ShowS #show :: Dim k ds -> String #showList :: [Dim k ds] -> ShowS #

dimVal :: Dim x -> Int Source #

Get value of type-level dim at runtime. Gives a product of all dimensions if is a list.

totalDim :: forall ds proxy. Dimensions ds => proxy ds -> Int Source #

Product of all dimension sizes.

fromInt :: forall m. KnownDim m => Int -> Maybe (Dim (XN m)) Source #

Get runtime-known dim and make sure it is not smaller than the given Nat.

data SomeDims Source #

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

Constructors

 SomeDims (Dim ns)

Instances

 Source # Methods Source # Methods(<) :: SomeDims -> SomeDims -> Bool #(>) :: SomeDims -> SomeDims -> Bool # Source # MethodsshowList :: [SomeDims] -> ShowS #

data SomeDim Source #

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

Constructors

 SomeDim (Dim n)

Similar to someNatVal, but for a single dimension

Convert a list of ints into unknown type-level Dimensions list

sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs)) Source #

We either get evidence that this function was instantiated with the same type-level Dimensions, or Nothing.

compareDim :: Dim as -> Dim 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).

inSpaceOf :: a ds -> b ds -> a ds Source #

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

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.

# Dimension constraints

class Dimensions ds where Source #

Minimal complete definition

dim

Methods

dim :: Dim ds Source #

Dimensionality of our space

Instances

 Dimensions ([] Nat) Source # Methodsdim :: Dim [Nat] [Nat] Source # (KnownDim d, Dimensions ds) => Dimensions ((:) Nat d ds) Source # Methodsdim :: Dim [Nat] ((Nat ': d) ds) Source #

class KnownDim n where Source #

This class gives the int associated with a type-level natural. Valid known dim must be not less than 0.

Minimal complete definition

dimVal'

Methods

Get value of type-level dim at runtime

Instances

 KnownNat n => KnownDim n Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods Source # Methods KnownDim 10 Source # Methods KnownDim 11 Source # Methods KnownDim 12 Source # Methods KnownDim 13 Source # Methods KnownDim 14 Source # Methods KnownDim 15 Source # Methods KnownDim 16 Source # Methods KnownDim 17 Source # Methods KnownDim 18 Source # Methods KnownDim 19 Source # Methods KnownDim 20 Source # Methods

type family KnownDims (ns :: [Nat]) :: Constraint where ... Source #

A constraint family that makes sure all subdimensions are known.

Equations

 KnownDims '[] = () KnownDims (x ': xs) = (KnownDim x, KnownDims xs)

# 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 WrapDims (x :: [k]) :: [XNat] where ... Source #

Treat Dims or XDims uniformly as XDims

Equations

 WrapDims ('[] :: [Nat]) = '[] WrapDims ('[] :: [XNat]) = '[] WrapDims (n ': ns :: [Nat]) = N n ': WrapDims ns WrapDims (xns :: [XNat]) = xns

type family UnwrapDims (xns :: [k]) :: [Nat] where ... Source #

Treat Dims or XDims uniformly as Dims

Equations

 UnwrapDims ('[] :: [Nat]) = '[] UnwrapDims ('[] :: [XNat]) = '[] UnwrapDims (N x ': xs) = x ': UnwrapDims xs UnwrapDims (XN _ ': _) = TypeError (Text "Cannot unwrap dimension XN into Nat" :: Text "(dimension is not known at compile time)")

type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where ... Source #

Unify usage of XNat and Nat. This is useful in function and type definitions. Mainly used in the definition of Dim.

Equations

 ConsDim (x :: Nat) (xs :: [Nat]) = x ': xs ConsDim (x :: Nat) (xs :: [XNat]) = N x ': xs ConsDim (XN m) (xs :: [XNat]) = XN m ': xs

type family NatKind ks k :: Constraint where ... Source #

Constraint on kinds; makes sure that the second argument kind is Nat if the first is a list of Nats.

Equations

 NatKind [Nat] l = l ~ Nat NatKind [XNat] Nat = () NatKind [XNat] XNat = () NatKind ks k = ks ~ [k]

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

FixedDim tries not to inspect content of ns and construct it based only on xns when it is possible. This means it does not check if XN m <= n.

Equations

 FixedDim '[] _ = '[] FixedDim (N n ': xs) ns = n ': FixedDim xs (Tail ns) FixedDim (XN _ ': xs) ns = Head ns ': FixedDim xs (Tail ns)

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

FixedXDim tries not to inspect content of xns and construct it based only on ns when it is possible. This means it does not check if XN m <= n.

Equations

 FixedXDim _ '[] = '[] FixedXDim xs (n ': ns) = WrapNat (Head xs) n ': FixedXDim (Tail xs) ns

type family WrapNat (xn :: XNat) (n :: Nat) :: XNat where ... Source #

WrapNat tries not to inspect content of xn and construct it based only on n when it is possible. This means it does not check if XN m <= n.

Equations

 WrapNat (XN m) n = XN m WrapNat _ n = N n

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.

Equations

 0 :< _ = '[] 1 :< ns = ns n :< ns = n :+ ns

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.

Equations

 _ >: 0 = '[] ns >: 1 = ns ns >: n = ns +: n

# Inference of dimension evidence

inferDimensions :: forall ds. (KnownDims ds, FiniteList ds) => Evidence (Dimensions ds) Source #

Infer Dimensions given that the list is KnownDims and finite

inferDimKnownDims :: forall ds. Dimensions ds => Evidence (KnownDims ds) Source #

Dimensions implies KnownDims

inferDimFiniteList :: forall ds. Dimensions ds => Evidence (FiniteList ds) Source #

Dimensions implies FiniteList

inferTailDimensions :: forall ds. Dimensions ds => Maybe (Evidence (Dimensions (Tail ds))) Source #

Infer that tail list is also Dimensions

inferConcatDimensions :: forall as bs. (Dimensions as, Dimensions bs) => Evidence (Dimensions (as ++ bs)) Source #

Infer that concatenation is also Dimensions

inferPrefixDimensions :: forall bs asbs. (IsSuffix bs asbs ~ True, Dimensions bs, Dimensions asbs) => Evidence (Dimensions (Prefix bs asbs)) Source #

Infer that prefix is also Dimensions

inferSuffixDimensions :: forall as asbs. (IsPrefix as asbs ~ True, Dimensions as, Dimensions asbs) => Evidence (Dimensions (Suffix as asbs)) Source #

Infer that suffix is also Dimensions

inferSnocDimensions :: forall xs z. (KnownDim z, Dimensions xs) => Evidence (Dimensions (xs +: z)) Source #

Make snoc almost as good as cons

inferInitDimensions :: forall xs. Dimensions xs => Maybe (Evidence (Dimensions (Init xs))) Source #

Init of the list is also Dimensions

inferTakeNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Take n xs)) Source #

Take KnownDim of the list is also Dimensions

inferDropNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Drop n xs)) Source #

Drop KnownDim of the list is also Dimensions

inferReverseDimensions :: forall xs. Dimensions xs => Evidence (Dimensions (Reverse xs)) Source #

Reverse of the list is also Dimensions

reifyDimensions :: forall ds. Dim ds -> Evidence (Dimensions ds) Source #

Use the given Dim ds to create an instance of Dimensions ds dynamically.

# Cons and Snoc inference

inferUnSnocDimensions :: forall ds. Dimensions ds => Maybe (Evidence (SnocDimensions ds)) Source #

Init of the dimension list is also Dimensions, and the last dimension is KnownDim.

type SnocDimensions xs = (xs ~ (Init xs +: Last xs), xs ~ (Init xs ++ '[Last xs]), IsPrefix (Init xs) xs ~ True, IsSuffix '[Last xs] xs ~ True, Suffix (Init xs) xs ~ '[Last xs], Prefix '[Last xs] xs ~ Init xs, Dimensions (Init xs), KnownDim (Last xs)) Source #

Various evidence for the Snoc operation.

inferUnConsDimensions :: forall ds. Dimensions ds => Maybe (Evidence (ConsDimensions ds)) Source #

Tail of the dimension list is also Dimensions, and the head dimension is KnownDim.

type ConsDimensions xs = (xs ~ (Head xs :+ Tail xs), xs ~ ('[Head xs] ++ Tail xs), IsPrefix '[Head xs] xs ~ True, IsSuffix (Tail xs) xs ~ True, Suffix '[Head xs] xs ~ Tail xs, Prefix (Tail xs) xs ~ '[Head xs], Dimensions (Tail xs), KnownDim (Head xs)) Source #

Various evidence for the Snoc operation.