Numeric.Dimensions.Dim

Dimension data types

data Nat

data XNat

type XN n

type N n

data Dim ns

dimVal

totalDim

fromInt

data SomeDims

data SomeDim

someDimVal

someDimsVal

sameDim

compareDim

inSpaceOf

asSpaceOf

Dimension constraints

class Dimensions ds

class KnownDim n

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

Type-level programming

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

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

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

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

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

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

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

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

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

type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where ...

type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where ...

Inference of dimension evidence

inferDimensions

inferDimKnownDims

inferDimFiniteList

inferTailDimensions

inferConcatDimensions

inferPrefixDimensions

inferSuffixDimensions

inferSnocDimensions

inferInitDimensions

inferTakeNDimensions

inferDropNDimensions

inferReverseDimensions

reifyDimensions

Cons and Snoc inference

inferUnSnocDimensions

type SnocDimensions xs

inferUnConsDimensions

type ConsDimensions xs