dimensions-2.1.1.0: Safe type-level dimensionality for multidimensional data.
Copyright(c) Artem Chirkin
LicenseBSD3
Safe HaskellNone
LanguageHaskell2010

Data.Type.Lits

Description

A Mixture of TypeLits and TypeNats with Nats represented as Natural at runtime, plus some helper functions of our own.

Synopsis

Kinds

data Nat #

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

Instances

Instances details
KnownDimKind Nat Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Dimensions ns => BoundedDims (ns :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dimsBound :: Dims (DimsBound ns) Source #

constrainDims :: forall k (ys :: [k]). Dims ys -> Maybe (Dims ns) Source #

KnownDim n => BoundedDim (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound n :: Nat Source #

Methods

dimBound :: Dim (DimBound n) Source #

constrainDim :: forall k (y :: k). Dim y -> Maybe (Dim n) Source #

KnownNat n => KnownDim (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim n Source #

KnownDim 0 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 0 Source #

KnownDim 1 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 1 Source #

KnownDim 2 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 2 Source #

KnownDim 3 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 3 Source #

KnownDim 4 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 4 Source #

KnownDim 5 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 5 Source #

KnownDim 6 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 6 Source #

KnownDim 7 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 7 Source #

KnownDim 8 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 8 Source #

KnownDim 9 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 9 Source #

KnownDim 10 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 10 Source #

KnownDim 11 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 11 Source #

KnownDim 12 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 12 Source #

KnownDim 13 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 13 Source #

KnownDim 14 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 14 Source #

KnownDim 15 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 15 Source #

KnownDim 16 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 16 Source #

KnownDim 17 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 17 Source #

KnownDim 18 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 18 Source #

KnownDim 19 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 19 Source #

KnownDim 20 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 20 Source #

KnownDim 21 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 21 Source #

KnownDim 22 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 22 Source #

KnownDim 23 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 23 Source #

KnownDim 24 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 24 Source #

KnownDim 25 Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dim :: Dim 25 Source #

KnownDimType (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dimType :: DimType n Source #

Class (KnownNat n) (KnownDim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

cls :: KnownDim n :- KnownNat n #

KnownDim n => Enum (Idx n) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

succ :: Idx n -> Idx n #

pred :: Idx n -> Idx n #

toEnum :: Int -> Idx n #

fromEnum :: Idx n -> Int #

enumFrom :: Idx n -> [Idx n] #

enumFromThen :: Idx n -> Idx n -> [Idx n] #

enumFromTo :: Idx n -> Idx n -> [Idx n] #

enumFromThenTo :: Idx n -> Idx n -> Idx n -> [Idx n] #

Eq (Dim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

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

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

Eq (Dims ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

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

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

Typeable d => Data (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

gfoldl :: (forall d0 b. Data d0 => c (d0 -> b) -> d0 -> c b) -> (forall g. g -> c g) -> Dim d -> c (Dim d) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dim d) #

toConstr :: Dim d -> Constr #

dataTypeOf :: Dim d -> DataType #

dataCast1 :: Typeable t => (forall d0. Data d0 => c (t d0)) -> Maybe (c (Dim d)) #

dataCast2 :: Typeable t => (forall d0 e. (Data d0, Data e) => c (t d0 e)) -> Maybe (c (Dim d)) #

gmapT :: (forall b. Data b => b -> b) -> Dim d -> Dim d #

gmapQl :: (r -> r' -> r) -> r -> (forall d0. Data d0 => d0 -> r') -> Dim d -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d0. Data d0 => d0 -> r') -> Dim d -> r #

gmapQ :: (forall d0. Data d0 => d0 -> u) -> Dim d -> [u] #

gmapQi :: Int -> (forall d0. Data d0 => d0 -> u) -> Dim d -> u #

gmapM :: Monad m => (forall d0. Data d0 => d0 -> m d0) -> Dim d -> m (Dim d) #

gmapMp :: MonadPlus m => (forall d0. Data d0 => d0 -> m d0) -> Dim d -> m (Dim d) #

gmapMo :: MonadPlus m => (forall d0. Data d0 => d0 -> m d0) -> Dim d -> m (Dim d) #

KnownDim n => Num (Idx n) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

(+) :: Idx n -> Idx n -> Idx n #

(-) :: Idx n -> Idx n -> Idx n #

(*) :: Idx n -> Idx n -> Idx n #

negate :: Idx n -> Idx n #

abs :: Idx n -> Idx n #

signum :: Idx n -> Idx n #

fromInteger :: Integer -> Idx n #

Ord (Dim n) Source # 
Instance details

Defined in Numeric.Dimensions.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) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

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 d => Generic (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Associated Types

type Rep (Dim d) :: Type -> Type #

Methods

from :: Dim d -> Rep (Dim d) x #

to :: Rep (Dim d) x -> Dim d #

type DimBound (n :: Nat) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimBound (n :: Nat) = n
type Rep (Dim d) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type Rep (Dim d) = D1 ('MetaData "Dim" "Numeric.Dim" "dimensions" 'False) (C1 ('MetaCons (AppendSymbol "D" (ShowNat d)) 'PrefixI 'False) (U1 :: Type -> Type))

data Symbol #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

Instances details
SingKind Symbol

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Associated Types

type DemoteRep Symbol

Methods

fromSing :: forall (a :: Symbol). Sing a -> DemoteRep Symbol

KnownSymbol a => SingI (a :: Symbol)

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Methods

sing :: Sing a

type DemoteRep Symbol 
Instance details

Defined in GHC.Generics

type DemoteRep Symbol = String
data Sing (s :: Symbol) 
Instance details

Defined in GHC.Generics

data Sing (s :: Symbol) where

type KindOf (t :: k) = k Source #

Get the kind of a given type. Useful when we don't want to introduce another type parameter into a type signature (because the kind is determined by the type), but need to have some constraints on the type's kind.

type KindOfEl (ts :: [k]) = k Source #

Get the kind of a given list type. Useful when we don't want to introduce another type parameter into a type signature (because the kind is determined by the type), but need to have some constraints on the type's kind.

Linking type and value level

class KnownNat (n :: Nat) #

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: base-4.7.0.0

Minimal complete definition

natSing

Instances

Instances details
Class (KnownNat n) (KnownDim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

cls :: KnownDim n :- KnownNat n #

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural #

Since: base-4.10.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural #

Since: base-4.10.0.0

class KnownSymbol (n :: Symbol) #

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: base-4.7.0.0

Minimal complete definition

symbolSing

symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String #

Since: base-4.7.0.0

symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String #

Since: base-4.8.0.0

data SomeNat #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n) 

Instances

Instances details
Eq SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool #

(/=) :: SomeNat -> SomeNat -> Bool #

Ord SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Read SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Show SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

data SomeSymbol #

This type represents unknown type-level symbols.

Constructors

KnownSymbol n => SomeSymbol (Proxy n)

Since: base-4.7.0.0

Instances

Instances details
Eq SomeSymbol

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Ord SomeSymbol

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Read SomeSymbol

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Show SomeSymbol

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

someNatVal :: Natural -> SomeNat #

Convert an integer into an unknown type-level natural.

Since: base-4.10.0.0

someSymbolVal :: String -> SomeSymbol #

Convert a string into an unknown type-level symbol.

Since: base-4.7.0.0

sameNat :: forall (a :: Nat) (b :: Nat). (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

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

Since: base-4.7.0.0

sameSymbol :: forall (a :: Symbol) (b :: Symbol). (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

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

Since: base-4.7.0.0

Functions on type literals

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 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 (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

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

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Log2 (a :: Nat) :: Nat where ... #

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type Min (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b) Source #

Miminum among two type-level naturals.

type Max (a :: Nat) (b :: Nat) = Max' a b (CmpNat a b) Source #

Maximum among two type-level naturals.

type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ... #

Concatenation of type-level symbols.

Since: base-4.10.0.0

type family ShowNat (n :: Nat) :: Symbol where ... Source #

Convert a type-level Nat into a type-level Symbol.

Equations

ShowNat 0 = "0" 
ShowNat 1 = "1" 
ShowNat 2 = "2" 
ShowNat 3 = "3" 
ShowNat 4 = "4" 
ShowNat 5 = "5" 
ShowNat 6 = "6" 
ShowNat 7 = "7" 
ShowNat 8 = "8" 
ShowNat 9 = "9" 
ShowNat d = AppendSymbol (ShowNat (Div d 10)) (ShowNat (Mod d 10)) 

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 CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... #

Comparison of type-level symbols, as a function.

Since: base-4.7.0.0

type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b) Source #

Comparison of type-level naturals, as a constraint.

data SOrdering :: Ordering -> Type where Source #

Singleton-style version of Ordering. Pattern-match againts its constructor to witness the result of type-level comparison.

Constructors

SLT :: SOrdering 'LT 
SEQ :: SOrdering 'EQ 
SGT :: SOrdering 'GT 

cmpNat :: forall (a :: Nat) (b :: Nat) (proxy :: Nat -> Type). (KnownNat a, KnownNat b) => proxy a -> proxy b -> SOrdering (CmpNat a b) Source #

Pattern-match against the result of this function to get the evidence of comparing type-level Nats.

cmpSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy :: Symbol -> Type). (KnownSymbol a, KnownSymbol b) => proxy a -> proxy b -> SOrdering (CmpSymbol a b) Source #

Pattern-match against the result of this function to get the evidence of comparing type-level Symbols.

User-defined type errors

type family TypeError (a :: ErrorMessage) :: b where ... #

The type-level equivalent of error.

The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

Since: base-4.9.0.0

data ErrorMessage #

A description of a custom type error.

Constructors

Text Symbol

Show the text as is.

ShowType t

Pretty print the type. ShowType :: k -> ErrorMessage

ErrorMessage :<>: ErrorMessage infixl 6

Put two pieces of error message next to each other.

ErrorMessage :$$: ErrorMessage infixl 5

Stack two pieces of error message on top of each other.