Numeric.Dim

This module is based on TypeLits and re-exports its functionality. It provides KnownDim class that is similar to KnownNat, but keeps Words instead of Integers; 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.

Type level numbers that can be unknown.

data XNat

Either known or unknown at compile-time natural number

Constructors

XN Nat

N Nat

Instances

KnownDimKind XNat

Defined in Numeric.Dim

Methods

dimKind :: DimKind XNat

KnownDim n => KnownDim (N n :: XNat)

Defined in Numeric.Dim

Methods

dim :: Dim (N n)

XDimensions ([] :: [XNat])

Defined in Numeric.Dimensions.Dims

Methods

constrainDims :: Dims ds -> Maybe (Dims [])

Eq (Dim x)

Defined in Numeric.Dim

Methods

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

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

Eq (Dims ds)

Defined in Numeric.Dimensions.Dims

Methods

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

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

Ord (Dim x)

Defined in Numeric.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)

Defined in Numeric.Dimensions.Dims

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 m => Read (Dim (XN m))

Defined in Numeric.Dim

Methods

readsPrec :: Int -> ReadS (Dim (XN m))

readList :: ReadS [Dim (XN m)]

readPrec :: ReadPrec (Dim (XN m))

readListPrec :: ReadPrec [Dim (XN m)]

(XDimensions xs, KnownDim n) => XDimensions (N n ': xs)

Defined in Numeric.Dimensions.Dims

Methods

constrainDims :: Dims ds -> Maybe (Dims (N n ': xs))

(XDimensions xs, KnownDim m) => XDimensions (XN m ': xs)

Defined in Numeric.Dimensions.Dims

Methods

constrainDims :: Dims ds -> Maybe (Dims (XN m ': xs))

type XN (n :: Nat) = XN n

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

type N (n :: Nat) = N n

Known natural number

data XNatType :: XNat -> Type where

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

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 Dim :: forall (n :: k). () => KnownDim n => Dim n

Independently of the kind of type-level number, construct an instance of KnownDim from it.

Match against this pattern to bring KnownDim instance into scope when you don't know the kind of the Dim parameter.

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

Same as Dim pattern, but constrained to Nat kind.

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

Instances

Dimensions ds => Bounded (Dims ds)

Defined in Numeric.Dimensions.Dims

Methods

minBound :: Dims ds

maxBound :: Dims ds

Eq (Dim n)

Defined in Numeric.Dim

Methods

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

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

Eq (Dim x)

Defined in Numeric.Dim

Methods

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

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

Eq (Dims ds)

Defined in Numeric.Dimensions.Dims

Methods

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

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

Eq (Dims ds)

Defined in Numeric.Dimensions.Dims

Methods

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

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

Ord (Dim n)

Defined in Numeric.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)

Defined in Numeric.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)

Defined in Numeric.Dimensions.Dims

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)

Defined in Numeric.Dimensions.Dims

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 m => Read (Dim (XN m))

Defined in Numeric.Dim

Methods

readsPrec :: Int -> ReadS (Dim (XN m))

readList :: ReadS [Dim (XN m)]

readPrec :: ReadPrec (Dim (XN m))

readListPrec :: ReadPrec [Dim (XN m)]

Show (Dim x)

Defined in Numeric.Dim

Methods

showsPrec :: Int -> Dim x -> ShowS

show :: Dim x -> String

showList :: [Dim x] -> ShowS

Show (Dims xs)

Defined in Numeric.Dimensions.Dims

Methods

showsPrec :: Int -> Dims xs -> ShowS

show :: Dims xs -> String

showList :: [Dims xs] -> ShowS

type SomeDim = Dim (XN 0)

Same as SomeNat

class KnownDim (n :: k) where

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

Minimal complete definition

dim

Methods

dim :: Dim n

Get value of type-level dim at runtime.

Note, this function is supposed to be used with TypeApplications, and the KnownDim class has varying kind of the parameter; thus, the function has two type paremeters (kind and type of n). For example, you can type:

>>> :set -XTypeApplications
>>> :set -XDataKinds
>>> :t dim @Nat @3
dim @Nat @3 :: Dim 3

>>> :set -XTypeOperators
>>> :t dim @_ @(13 - 6)
dim @_ @(13 - 6) :: Dim 7

>>> :t dim @_ @(N 17)
dim @_ @(N 17) :: Dim (N 17)

Instances

KnownNat n => KnownDim (n :: Nat)

Defined in Numeric.Dim

Methods

dim :: Dim n

KnownDim 0

Defined in Numeric.Dim

Methods

dim :: Dim 0

KnownDim 1

Defined in Numeric.Dim

Methods

dim :: Dim 1

KnownDim 2

Defined in Numeric.Dim

Methods

dim :: Dim 2

KnownDim 3

Defined in Numeric.Dim

Methods

dim :: Dim 3

KnownDim 4

Defined in Numeric.Dim

Methods

dim :: Dim 4

KnownDim 5

Defined in Numeric.Dim

Methods

dim :: Dim 5

KnownDim 6

Defined in Numeric.Dim

Methods

dim :: Dim 6

KnownDim 7

Defined in Numeric.Dim

Methods

dim :: Dim 7

KnownDim 8

Defined in Numeric.Dim

Methods

dim :: Dim 8

KnownDim 9

Defined in Numeric.Dim

Methods

dim :: Dim 9

KnownDim 10

Defined in Numeric.Dim

Methods

dim :: Dim 10

KnownDim 11

Defined in Numeric.Dim

Methods

dim :: Dim 11

KnownDim 12

Defined in Numeric.Dim

Methods

dim :: Dim 12

KnownDim 13

Defined in Numeric.Dim

Methods

dim :: Dim 13

KnownDim 14

Defined in Numeric.Dim

Methods

dim :: Dim 14

KnownDim 15

Defined in Numeric.Dim

Methods

dim :: Dim 15

KnownDim 16

Defined in Numeric.Dim

Methods

dim :: Dim 16

KnownDim 17

Defined in Numeric.Dim

Methods

dim :: Dim 17

KnownDim 18

Defined in Numeric.Dim

Methods

dim :: Dim 18

KnownDim 19

Defined in Numeric.Dim

Methods

dim :: Dim 19

KnownDim 20

Defined in Numeric.Dim

Methods

dim :: Dim 20

KnownDim n => KnownDim (N n :: XNat)

Defined in Numeric.Dim

Methods

dim :: Dim (N n)

class KnownXNatType (n :: XNat) where

Find out the type of XNat constructor

Minimal complete definition

xNatType

Methods

xNatType :: XNatType n

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

Instances

KnownXNatType (XN n)

Defined in Numeric.Dim

Methods

xNatType :: XNatType (XN n)

KnownXNatType (N n)

Defined in Numeric.Dim

Methods

xNatType :: XNatType (N n)

dimVal :: Dim (x :: k) -> Word

Similar to natVal from TypeLits, but returns Word.

dimVal' :: forall n. KnownDim n => Word

Similar to natVal from TypeLits, but returns Word.

someDimVal :: Word -> SomeDim

Similar to someNatVal from TypeLits.

sameDim :: forall (x :: Nat) (y :: Nat). Dim x -> Dim y -> Maybe (Evidence (x ~ y))

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 q. (KnownDim x, KnownDim y) => p x -> q y -> Maybe (Evidence (x ~ y))

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

compareDim :: Dim a -> Dim b -> Ordering

Ordering of dimension values.

compareDim' :: forall a b p q. (KnownDim a, KnownDim b) => p a -> q b -> Ordering

Ordering of dimension values.

constrain :: forall (m :: Nat) x. KnownDim m => Dim x -> Maybe (Dim (XN m))

Change the minimum allowed size of a Dim (XN x), while testing if the value inside satisfies it.

constrainBy :: forall m x. Dim m -> Dim x -> Maybe (Dim (XN m))

constrain with explicitly-passed constraining Dim to avoid AllowAmbiguousTypes.

relax :: forall (m :: Nat) (n :: Nat). MinDim m n => Dim (XN n) -> Dim (XN m)

Decrease minimum allowed size of a Dim (XN x).

Simple Dim arithmetics

plusDim :: Dim n -> Dim m -> Dim (n + m)

minusDim :: MinDim m n => Dim n -> Dim m -> Dim (n - m)

minusDimM :: Dim n -> Dim m -> Maybe (Dim (n - m))

timesDim :: Dim n -> Dim m -> Dim (* n m)

powerDim :: Dim n -> Dim m -> Dim ((^) n m)

Re-export part of TypeLits for convenience

data Nat

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

Instances

KnownDimKind Nat

Defined in Numeric.Dim

Methods

dimKind :: DimKind Nat

KnownNat n => KnownDim (n :: Nat)

Defined in Numeric.Dim

Methods

dim :: Dim n

KnownDim 0

Defined in Numeric.Dim

Methods

dim :: Dim 0

KnownDim 1

Defined in Numeric.Dim

Methods

dim :: Dim 1

KnownDim 2

Defined in Numeric.Dim

Methods

dim :: Dim 2

KnownDim 3

Defined in Numeric.Dim

Methods

dim :: Dim 3

KnownDim 4

Defined in Numeric.Dim

Methods

dim :: Dim 4

KnownDim 5

Defined in Numeric.Dim

Methods

dim :: Dim 5

KnownDim 6

Defined in Numeric.Dim

Methods

dim :: Dim 6

KnownDim 7

Defined in Numeric.Dim

Methods

dim :: Dim 7

KnownDim 8

Defined in Numeric.Dim

Methods

dim :: Dim 8

KnownDim 9

Defined in Numeric.Dim

Methods

dim :: Dim 9

KnownDim 10

Defined in Numeric.Dim

Methods

dim :: Dim 10

KnownDim 11

Defined in Numeric.Dim

Methods

dim :: Dim 11

KnownDim 12

Defined in Numeric.Dim

Methods

dim :: Dim 12

KnownDim 13

Defined in Numeric.Dim

Methods

dim :: Dim 13

KnownDim 14

Defined in Numeric.Dim

Methods

dim :: Dim 14

KnownDim 15

Defined in Numeric.Dim

Methods

dim :: Dim 15

KnownDim 16

Defined in Numeric.Dim

Methods

dim :: Dim 16

KnownDim 17

Defined in Numeric.Dim

Methods

dim :: Dim 17

KnownDim 18

Defined in Numeric.Dim

Methods

dim :: Dim 18

KnownDim 19

Defined in Numeric.Dim

Methods

dim :: Dim 19

KnownDim 20

Defined in Numeric.Dim

Methods

dim :: Dim 20

Eq (Dim n)

Defined in Numeric.Dim

Methods

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

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

Eq (Dims ds)

Defined in Numeric.Dimensions.Dims

Methods

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

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

Ord (Dim n)

Defined in Numeric.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)

Defined in Numeric.Dimensions.Dims

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 family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

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 family MinDim (m :: Nat) (n :: Nat) :: Constraint where ...

Friendly error message if `m <= n` constraint is not satisfied. Use this type family instead of (<=) if possible or try inferDimLE function as the last resort.

Equations

MinDim m n = If (CmpNat m n == GT) (TypeError ((((((Text "Minimum Dim size constraint (" :<>: ShowType m) :<>: Text " <= ") :<>: ShowType n) :<>: Text ") is not satisfied.") :$$: (Text "Minimum Dim: " :<>: ShowType m)) :$$: (Text " Actual Dim: " :<>: ShowType n)) :: Constraint) (m <= n)

type family FixedDim (x :: XNat) (n :: Nat) :: Constraint where ...

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 = MinDim m b

inferDimLE :: forall m n. MinDim m n => Evidence (m <= n)

MinDim implies (<=), but this fact is not so clear to GHC. This function assures the type system that the relation takes place.

Inferring kind of type-level dimension

class KnownDimKind k where

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

Minimal complete definition

dimKind

Methods

dimKind :: DimKind k

Instances

KnownDimKind Nat

Defined in Numeric.Dim

Methods

dimKind :: DimKind Nat

KnownDimKind XNat

Defined in Numeric.Dim

Methods

dimKind :: DimKind XNat

data DimKind :: Type -> Type where

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.