dimensions-2.0.0.0: Safe type-level dimensionality for multidimensional data.

Copyright(c) Artem Chirkin
LicenseBSD3
Safe HaskellNone
LanguageHaskell2010

Data.Type.Lits

Contents

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
KnownDimKind Nat Source # 
Instance details

Defined in Numeric.Dimensions.Dim

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

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound ns :: [Nat] Source #

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

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound n :: Nat Source #

Dimensions ([] :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims [] Source #

Dimensions ds => Enum (Idxs ds) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

Methods

succ :: Idxs ds -> Idxs ds #

pred :: Idxs ds -> Idxs ds #

toEnum :: Int -> Idxs ds #

fromEnum :: Idxs ds -> Int #

enumFrom :: Idxs ds -> [Idxs ds] #

enumFromThen :: Idxs ds -> Idxs ds -> [Idxs ds] #

enumFromTo :: Idxs ds -> Idxs ds -> [Idxs ds] #

enumFromThenTo :: Idxs ds -> Idxs ds -> Idxs ds -> [Idxs ds] #

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 :: (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) #

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 #

(KnownDim d, Dimensions ds) => Dimensions (d ': ds) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims (d ': ds) Source #

type DimsBound (ns :: [Nat]) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

type DimsBound (ns :: [Nat]) = ns
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
SingKind Symbol

Since: base-4.9.0.0

Instance details

Defined in GHC.Generics

Associated Types

type DemoteRep Symbol :: Type

Methods

fromSing :: 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

data Sing (s :: Symbol) 
Instance details

Defined in GHC.Generics

data Sing (s :: Symbol) where
type DemoteRep Symbol 
Instance details

Defined in GHC.Generics

type DemoteRep Symbol = String

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
Class (KnownNat n) (KnownDim n) Source # 
Instance details

Defined in Numeric.Dimensions.Dim

Methods

cls :: KnownDim n :- KnownNat n #

natVal :: KnownNat n => proxy n -> Natural #

Since: base-4.10.0.0

natVal' :: 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 :: KnownSymbol n => proxy n -> String #

Since: base-4.7.0.0

symbolVal' :: KnownSymbol n => Proxy# n -> String #

Since: base-4.8.0.0

data SomeNat where #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat 
Instances
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 where #

This type represents unknown type-level symbols.

Constructors

SomeSymbol :: forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol

Since: base-4.7.0.0

Instances
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 :: (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 :: (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 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 where #

A description of a custom type error.

Constructors

Text :: forall. Symbol -> ErrorMessage

Show the text as is.

ShowType :: forall t. t -> ErrorMessage

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

(:<>:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 5

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