Numeric.Dim

This module is based on TypeLits and re-exports its functionality. It provides KnownDim class that is similar to KnownNat, but keeps Ints instead of Integers; Also it provides Dim data family serving as a customized Proxy type and 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

Methods

dimKind :: DimKind XNat

KnownDim Nat n => KnownDim XNat (N n)

Methods

dim :: Dim (N n) n

Eq (Dim XNat x)

Methods

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

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

Ord (Dim XNat x)

Methods

compare :: Dim XNat x -> Dim XNat x -> Ordering

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

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

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

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

max :: Dim XNat x -> Dim XNat x -> Dim XNat x

min :: Dim XNat x -> Dim XNat x -> Dim XNat x

KnownDim Nat m => Read (Dim XNat (XN m))

Methods

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

readList :: ReadS [Dim XNat (XN m)]

readPrec :: ReadPrec (Dim XNat (XN m))

readListPrec :: ReadPrec [Dim XNat (XN m)]

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

Eq (Dim Nat n)

Methods

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

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

Eq (Dim XNat x)

Methods

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

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

Ord (Dim Nat n)

Methods

compare :: Dim Nat n -> Dim Nat n -> Ordering

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

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

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

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

max :: Dim Nat n -> Dim Nat n -> Dim Nat n

min :: Dim Nat n -> Dim Nat n -> Dim Nat n

Ord (Dim XNat x)

Methods

compare :: Dim XNat x -> Dim XNat x -> Ordering

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

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

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

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

max :: Dim XNat x -> Dim XNat x -> Dim XNat x

min :: Dim XNat x -> Dim XNat x -> Dim XNat x

KnownDim Nat m => Read (Dim XNat (XN m))

Methods

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

readList :: ReadS [Dim XNat (XN m)]

readPrec :: ReadPrec (Dim XNat (XN m))

readListPrec :: ReadPrec [Dim XNat (XN m)]

Show (Dim k x)

Methods

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

show :: Dim k x -> String

showList :: [Dim k x] -> 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 Nat n

Methods

dim :: Dim n n

KnownDim Nat 0

Methods

dim :: Dim 0 n

KnownDim Nat 1

Methods

dim :: Dim 1 n

KnownDim Nat 2

Methods

dim :: Dim 2 n

KnownDim Nat 3

Methods

dim :: Dim 3 n

KnownDim Nat 4

Methods

dim :: Dim 4 n

KnownDim Nat 5

Methods

dim :: Dim 5 n

KnownDim Nat 6

Methods

dim :: Dim 6 n

KnownDim Nat 7

Methods

dim :: Dim 7 n

KnownDim Nat 8

Methods

dim :: Dim 8 n

KnownDim Nat 9

Methods

dim :: Dim 9 n

KnownDim Nat 10

Methods

dim :: Dim 10 n

KnownDim Nat 11

Methods

dim :: Dim 11 n

KnownDim Nat 12

Methods

dim :: Dim 12 n

KnownDim Nat 13

Methods

dim :: Dim 13 n

KnownDim Nat 14

Methods

dim :: Dim 14 n

KnownDim Nat 15

Methods

dim :: Dim 15 n

KnownDim Nat 16

Methods

dim :: Dim 16 n

KnownDim Nat 17

Methods

dim :: Dim 17 n

KnownDim Nat 18

Methods

dim :: Dim 18 n

KnownDim Nat 19

Methods

dim :: Dim 19 n

KnownDim Nat 20

Methods

dim :: Dim 20 n

KnownDim Nat n => KnownDim XNat (N n)

Methods

dim :: Dim (N 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)

Methods

xNatType :: XNatType (XN n)

KnownXNatType (N n)

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

Methods

dimKind :: DimKind Nat

KnownNat n => KnownDim Nat n

Methods

dim :: Dim n n

KnownDim Nat 0

Methods

dim :: Dim 0 n

KnownDim Nat 1

Methods

dim :: Dim 1 n

KnownDim Nat 2

Methods

dim :: Dim 2 n

KnownDim Nat 3

Methods

dim :: Dim 3 n

KnownDim Nat 4

Methods

dim :: Dim 4 n

KnownDim Nat 5

Methods

dim :: Dim 5 n

KnownDim Nat 6

Methods

dim :: Dim 6 n

KnownDim Nat 7

Methods

dim :: Dim 7 n

KnownDim Nat 8

Methods

dim :: Dim 8 n

KnownDim Nat 9

Methods

dim :: Dim 9 n

KnownDim Nat 10

Methods

dim :: Dim 10 n

KnownDim Nat 11

Methods

dim :: Dim 11 n

KnownDim Nat 12

Methods

dim :: Dim 12 n

KnownDim Nat 13

Methods

dim :: Dim 13 n

KnownDim Nat 14

Methods

dim :: Dim 14 n

KnownDim Nat 15

Methods

dim :: Dim 15 n

KnownDim Nat 16

Methods

dim :: Dim 16 n

KnownDim Nat 17

Methods

dim :: Dim 17 n

KnownDim Nat 18

Methods

dim :: Dim 18 n

KnownDim Nat 19

Methods

dim :: Dim 19 n

KnownDim Nat 20

Methods

dim :: Dim 20 n

Eq (Dim Nat n)

Methods

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

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

Ord (Dim Nat n)

Methods

compare :: Dim Nat n -> Dim Nat n -> Ordering

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

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

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

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

max :: Dim Nat n -> Dim Nat n -> Dim Nat n

min :: Dim Nat n -> Dim Nat n -> Dim Nat n

type (==) Nat a b

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

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

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

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

Addition of type-level naturals.

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

Subtraction of type-level naturals.

Since: 4.7.0.0

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

Multiplication of type-level naturals.

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

Exponentiation of type-level naturals.

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

Methods

dimKind :: DimKind Nat

KnownDimKind XNat

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.