Numeric.Dimensions.Dim

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

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)

Methods

dim :: Dim [Nat] [Nat]

Dimensions ds => Bounded (Dim [Nat] ds)

Methods

minBound :: Dim [Nat] ds

maxBound :: Dim [Nat] ds

(KnownDim d, Dimensions ds) => Dimensions ((:) Nat d ds)

Methods

dim :: Dim [Nat] ((Nat ': d) ds)

type (==) Nat a b

type (==) Nat a b = EqNat a b

data XNat

Either known or unknown at compile-time natural number

Instances

XDimensions ([] XNat)

Methods

wrapDim :: ([XNat] ~ FixedXDim [XNat] ds) [XNat] => Dim [Nat] ds -> Dim [XNat] [XNat]

XDimensions xs => XDimensions ((:) XNat (N n) xs)

Methods

wrapDim :: ([XNat] ~ FixedXDim ((XNat ': N n) xs) ds) ((XNat ': N n) xs) => Dim [Nat] ds -> Dim [XNat] ((XNat ': N n) xs)

XDimensions xs => XDimensions ((:) XNat (XN m) xs)

Methods

wrapDim :: ([XNat] ~ FixedXDim ((XNat ': XN m) xs) ds) ((XNat ': XN m) xs) => Dim [Nat] ds -> Dim [XNat] ((XNat ': XN m) xs)

type XN n = XN n

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

type N n = N n

Known natural number

data Dim ns where

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)

Methods

minBound :: Dim [Nat] ds

maxBound :: Dim [Nat] ds

Eq (Dim k ds)

Methods

(==) :: Dim k ds -> Dim k ds -> Bool

(/=) :: Dim k ds -> Dim k ds -> Bool

Ord (Dim k ds)

Methods

compare :: 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)

Methods

showsPrec :: Int -> Dim k ds -> ShowS

show :: Dim k ds -> String

showList :: [Dim k ds] -> ShowS

dimVal :: Dim x -> Int

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

Product of all dimension sizes.

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

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

data SomeDims

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

Constructors

SomeDims (Dim ns)

Instances

Eq SomeDims

Methods

(==) :: SomeDims -> SomeDims -> Bool

(/=) :: SomeDims -> SomeDims -> Bool

Ord SomeDims

Methods

compare :: SomeDims -> SomeDims -> Ordering

(<) :: SomeDims -> SomeDims -> Bool

(<=) :: SomeDims -> SomeDims -> Bool

(>) :: SomeDims -> SomeDims -> Bool

(>=) :: SomeDims -> SomeDims -> Bool

max :: SomeDims -> SomeDims -> SomeDims

min :: SomeDims -> SomeDims -> SomeDims

Show SomeDims

Methods

showsPrec :: Int -> SomeDims -> ShowS

show :: SomeDims -> String

showList :: [SomeDims] -> ShowS

data SomeDim

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

Constructors

SomeDim (Dim n)

someDimVal :: Int -> Maybe SomeDim

Similar to someNatVal, but for a single dimension

someDimsVal :: [Int] -> Maybe SomeDims

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

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

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

compareDim :: Dim as -> Dim bs -> Ordering

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

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

Similar to asProxyTypeOf, Give a hint to type checker to fix the type of a function argument.

Dimension constraints

class Dimensions ds where

Minimal complete definition

dim

Methods

dim :: Dim ds

Dimensionality of our space

Instances

Dimensions ([] Nat)

Methods

dim :: Dim [Nat] [Nat]

(KnownDim d, Dimensions ds) => Dimensions ((:) Nat d ds)

Methods

dim :: Dim [Nat] ((Nat ': d) ds)

class KnownDim n where

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

dimVal' :: Int

Get value of type-level dim at runtime

Instances

KnownNat n => KnownDim n

Methods

dimVal' :: Int

KnownDim 0

Methods

dimVal' :: Int

KnownDim 1

Methods

dimVal' :: Int

KnownDim 2

Methods

dimVal' :: Int

KnownDim 3

Methods

dimVal' :: Int

KnownDim 4

Methods

dimVal' :: Int

KnownDim 5

Methods

dimVal' :: Int

KnownDim 6

Methods

dimVal' :: Int

KnownDim 7

Methods

dimVal' :: Int

KnownDim 8

Methods

dimVal' :: Int

KnownDim 9

Methods

dimVal' :: Int

KnownDim 10

Methods

dimVal' :: Int

KnownDim 11

Methods

dimVal' :: Int

KnownDim 12

Methods

dimVal' :: Int

KnownDim 13

Methods

dimVal' :: Int

KnownDim 14

Methods

dimVal' :: Int

KnownDim 15

Methods

dimVal' :: Int

KnownDim 16

Methods

dimVal' :: Int

KnownDim 17

Methods

dimVal' :: Int

KnownDim 18

Methods

dimVal' :: Int

KnownDim 19

Methods

dimVal' :: Int

KnownDim 20

Methods

dimVal' :: Int

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

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

Map Dims onto XDims (injective)

Equations

AsXDims '[] = '[]

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

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

Map XDims onto Dims (injective)

Equations

AsDims '[] = '[]

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

type family WrapDims (x :: [k]) :: [XNat] where ...

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

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

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

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

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

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

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

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

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)

Infer Dimensions given that the list is KnownDims and finite

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

Dimensions implies KnownDims

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

Dimensions implies FiniteList

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

Infer that tail list is also Dimensions

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

Infer that concatenation is also Dimensions

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

Infer that prefix is also Dimensions

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

Infer that suffix is also Dimensions

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

Make snoc almost as good as cons

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

Init of the list is also Dimensions

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

Take KnownDim of the list is also Dimensions

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

Drop KnownDim of the list is also Dimensions

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

Reverse of the list is also Dimensions

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

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

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

Various evidence for the Snoc operation.

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

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

Various evidence for the Snoc operation.