Data.Type.Lits

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

Kinds

data Nat

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

Instances

KnownDimKind Nat

Defined in Numeric.Dimensions.Dim

Methods

dimKind :: DimKind Nat

Dimensions ns => BoundedDims (ns :: [Nat])

Defined in Numeric.Dimensions.Dim

Associated Types

type DimsBound ns :: [Nat]

Methods

dimsBound :: Dims (DimsBound ns)

constrainDims :: Dims ys -> Maybe (Dims ns)

inferAllBoundedDims :: Dict (All BoundedDim ns, RepresentableList ns)

KnownDim n => BoundedDim (n :: Nat)

Defined in Numeric.Dimensions.Dim

Associated Types

type DimBound n :: Nat

Methods

dimBound :: Dim (DimBound n)

constrainDim :: Dim y -> Maybe (Dim n)

Dimensions ([] :: [Nat])

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims []

Dimensions ds => Enum (Idxs ds)

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)

Defined in Numeric.Dimensions.Dim

Methods

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

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

Eq (Dims ds)

Defined in Numeric.Dimensions.Dim

Methods

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

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

Typeable d => Data (Dim d)

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)

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)

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)

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)

Defined in Numeric.Dimensions.Dim

Methods

dims :: Dims (d ': ds)

type DimsBound (ns :: [Nat])

Defined in Numeric.Dimensions.Dim

type DimsBound (ns :: [Nat]) = ns

type DimBound (n :: Nat)

Defined in Numeric.Dimensions.Dim

type DimBound (n :: Nat) = n

type Rep (Dim d)

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

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

Defined in GHC.Generics

Methods

sing :: Sing a

data Sing (s :: Symbol)

Defined in GHC.Generics

data Sing (s :: Symbol) where

• SSym :: forall (s :: Symbol). KnownSymbol s => Sing s

type DemoteRep Symbol

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)

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

Defined in GHC.TypeNats

Methods

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

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

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering

(<) :: SomeNat -> SomeNat -> Bool

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

(>) :: SomeNat -> SomeNat -> Bool

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

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

Read SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

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

Defined in GHC.TypeLits

Methods

(==) :: SomeSymbol -> SomeSymbol -> Bool

(/=) :: SomeSymbol -> SomeSymbol -> Bool

Ord SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

compare :: SomeSymbol -> SomeSymbol -> Ordering

(<) :: SomeSymbol -> SomeSymbol -> Bool

(<=) :: SomeSymbol -> SomeSymbol -> Bool

(>) :: SomeSymbol -> SomeSymbol -> Bool

(>=) :: SomeSymbol -> SomeSymbol -> Bool

max :: SomeSymbol -> SomeSymbol -> SomeSymbol

min :: SomeSymbol -> SomeSymbol -> SomeSymbol

Read SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

readsPrec :: Int -> ReadS SomeSymbol

readList :: ReadS [SomeSymbol]

readPrec :: ReadPrec SomeSymbol

readListPrec :: ReadPrec [SomeSymbol]

Show SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

showsPrec :: Int -> SomeSymbol -> ShowS

show :: SomeSymbol -> String

showList :: [SomeSymbol] -> ShowS

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

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)

Comparison of type-level naturals, as a constraint.

data SOrdering :: Ordering -> Type where

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)

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)

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.