Copyright	(c) Artem Chirkin
License	BSD3
Maintainer	[email protected]
Safe Haskell	None
Language	Haskell2010

Numeric.Dim

Contents

Type level numbers that can be unknown.
Term level dimension
Simple Dim arithmetics
Re-export part of TypeLits for convenience
Inferring kind of type-level dimension

Description

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.

Synopsis

Type level numbers that can be unknown.

data XNat Source #

Either known or unknown at compile-time natural number

Constructors

XN Nat
N Nat

Instances

KnownDimKind XNat Source #
Methods dimKind :: DimKind XNat Source #
KnownDim Nat n => KnownDim XNat (N n) Source #
Methods dim :: Dim (N n) n Source #
Eq (Dim XNat x) Source #
Methods (==) :: Dim XNat x -> Dim XNat x -> Bool # (/=) :: Dim XNat x -> Dim XNat x -> Bool #
Ord (Dim XNat x) Source #
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)) Source #
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 Source #

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

type N (n :: Nat) = N n Source #

Known natural number

data XNatType :: XNat -> Type where Source #

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 Source #

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) Source #
Methods (==) :: Dim Nat n -> Dim Nat n -> Bool # (/=) :: Dim Nat n -> Dim Nat n -> Bool #
Eq (Dim XNat x) Source #
Methods (==) :: Dim XNat x -> Dim XNat x -> Bool # (/=) :: Dim XNat x -> Dim XNat x -> Bool #
Ord (Dim Nat n) Source #
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) Source #
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)) Source #
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) Source #
Methods showsPrec :: Int -> Dim k x -> ShowS # show :: Dim k x -> String # showList :: [Dim k x] -> ShowS #

type SomeDim = Dim (XN 0) Source #

Same as SomeNat

class KnownDim (n :: k) where Source #

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

Minimal complete definition

dim

Methods

dim :: Dim n Source #

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 Source #
Methods dim :: Dim n n Source #
KnownDim Nat 0 Source #
Methods dim :: Dim 0 n Source #
KnownDim Nat 1 Source #
Methods dim :: Dim 1 n Source #
KnownDim Nat 2 Source #
Methods dim :: Dim 2 n Source #
KnownDim Nat 3 Source #
Methods dim :: Dim 3 n Source #
KnownDim Nat 4 Source #
Methods dim :: Dim 4 n Source #
KnownDim Nat 5 Source #
Methods dim :: Dim 5 n Source #
KnownDim Nat 6 Source #
Methods dim :: Dim 6 n Source #
KnownDim Nat 7 Source #
Methods dim :: Dim 7 n Source #
KnownDim Nat 8 Source #
Methods dim :: Dim 8 n Source #
KnownDim Nat 9 Source #
Methods dim :: Dim 9 n Source #
KnownDim Nat 10 Source #
Methods dim :: Dim 10 n Source #
KnownDim Nat 11 Source #
Methods dim :: Dim 11 n Source #
KnownDim Nat 12 Source #
Methods dim :: Dim 12 n Source #
KnownDim Nat 13 Source #
Methods dim :: Dim 13 n Source #
KnownDim Nat 14 Source #
Methods dim :: Dim 14 n Source #
KnownDim Nat 15 Source #
Methods dim :: Dim 15 n Source #
KnownDim Nat 16 Source #
Methods dim :: Dim 16 n Source #
KnownDim Nat 17 Source #
Methods dim :: Dim 17 n Source #
KnownDim Nat 18 Source #
Methods dim :: Dim 18 n Source #
KnownDim Nat 19 Source #
Methods dim :: Dim 19 n Source #
KnownDim Nat 20 Source #
Methods dim :: Dim 20 n Source #
KnownDim Nat n => KnownDim XNat (N n) Source #
Methods dim :: Dim (N n) n Source #

class KnownXNatType (n :: XNat) where Source #

Find out the type of XNat constructor

Minimal complete definition

xNatType

Methods

xNatType :: XNatType n Source #

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

Instances

KnownXNatType (XN n) Source #
Methods xNatType :: XNatType (XN n) Source #
KnownXNatType (N n) Source #
Methods xNatType :: XNatType (N n) Source #

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

Similar to natVal from TypeLits, but returns Word.

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

Similar to natVal from TypeLits, but returns Word.

someDimVal :: Word -> SomeDim Source #

Similar to someNatVal from TypeLits.

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

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

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

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

Ordering of dimension values.

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

Ordering of dimension values.

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

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

constrain with explicitly-passed constraining Dim to avoid AllowAmbiguousTypes.

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

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

Simple Dim arithmetics

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

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

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

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

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

Re-export part of `TypeLits` for convenience

data Nat :: * #

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

Instances

KnownDimKind Nat Source #
Methods dimKind :: DimKind Nat Source #
KnownNat n => KnownDim Nat n Source #
Methods dim :: Dim n n Source #
KnownDim Nat 0 Source #
Methods dim :: Dim 0 n Source #
KnownDim Nat 1 Source #
Methods dim :: Dim 1 n Source #
KnownDim Nat 2 Source #
Methods dim :: Dim 2 n Source #
KnownDim Nat 3 Source #
Methods dim :: Dim 3 n Source #
KnownDim Nat 4 Source #
Methods dim :: Dim 4 n Source #
KnownDim Nat 5 Source #
Methods dim :: Dim 5 n Source #
KnownDim Nat 6 Source #
Methods dim :: Dim 6 n Source #
KnownDim Nat 7 Source #
Methods dim :: Dim 7 n Source #
KnownDim Nat 8 Source #
Methods dim :: Dim 8 n Source #
KnownDim Nat 9 Source #
Methods dim :: Dim 9 n Source #
KnownDim Nat 10 Source #
Methods dim :: Dim 10 n Source #
KnownDim Nat 11 Source #
Methods dim :: Dim 11 n Source #
KnownDim Nat 12 Source #
Methods dim :: Dim 12 n Source #
KnownDim Nat 13 Source #
Methods dim :: Dim 13 n Source #
KnownDim Nat 14 Source #
Methods dim :: Dim 14 n Source #
KnownDim Nat 15 Source #
Methods dim :: Dim 15 n Source #
KnownDim Nat 16 Source #
Methods dim :: Dim 16 n Source #
KnownDim Nat 17 Source #
Methods dim :: Dim 17 n Source #
KnownDim Nat 18 Source #
Methods dim :: Dim 18 n Source #
KnownDim Nat 19 Source #
Methods dim :: Dim 19 n Source #
KnownDim Nat 20 Source #
Methods dim :: Dim 20 n Source #
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 ... Source #

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

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

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 Source #

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

Minimal complete definition

dimKind

Methods

dimKind :: DimKind k Source #

Instances

KnownDimKind Nat Source #
Methods dimKind :: DimKind Nat Source #
KnownDimKind XNat Source #
Methods dimKind :: DimKind XNat Source #

data DimKind :: Type -> Type where Source #

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

Type level numbers that can be unknown.

Term level dimension

Simple Dim arithmetics

Re-export part of TypeLits for convenience

Inferring kind of type-level dimension

Re-export part of `TypeLits` for convenience