Safe Haskell  Trustworthy 

Language  Haskell2010 
GHC's DataKinds
language extension lifts data constructors, natural
numbers, and strings to the type level. This module provides the
primitives needed for working with typelevel numbers (the Nat
kind),
strings (the Symbol
kind), and characters (the Char
kind). It also defines the TypeError
type
family, a feature that makes use of typelevel strings to support user
defined type errors.
For now, this module is the API for working with typelevel literals.
However, please note that it is a work in progress and is subject to change.
Once the design of the DataKinds
feature is more stable, this will be
considered only an internal GHC module, and the programmer interface for
working with typelevel data will be defined in a separate library.
Since: base4.6.0.0
Synopsis
 data Natural
 type Nat = Natural
 data Symbol
 class KnownNat (n :: Nat)
 natVal :: forall n proxy. KnownNat n => proxy n > Integer
 natVal' :: forall n. KnownNat n => Proxy# n > Integer
 class KnownSymbol (n :: Symbol)
 symbolVal :: forall n proxy. KnownSymbol n => proxy n > String
 symbolVal' :: forall n. KnownSymbol n => Proxy# n > String
 class KnownChar (n :: Char)
 charVal :: forall n proxy. KnownChar n => proxy n > Char
 charVal' :: forall n. KnownChar n => Proxy# n > Char
 data SomeNat = forall n.KnownNat n => SomeNat (Proxy n)
 data SomeSymbol = forall n.KnownSymbol n => SomeSymbol (Proxy n)
 data SomeChar = forall n.KnownChar n => SomeChar (Proxy n)
 someNatVal :: Integer > Maybe SomeNat
 someSymbolVal :: String > SomeSymbol
 someCharVal :: Char > SomeChar
 sameNat :: (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Maybe (a :~: b)
 sameSymbol :: (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Maybe (a :~: b)
 sameChar :: (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > Maybe (a :~: b)
 data OrderingI a b where
 cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > OrderingI a b
 cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > OrderingI a b
 cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > OrderingI a b
 type (<=) x y = Assert (x <=? y) (LeErrMsg x y)
 type (<=?) m n = OrdCond (Compare m n) 'True 'True 'False
 type family (m :: Nat) + (n :: Nat) :: Nat
 type family (m :: Nat) * (n :: Nat) :: Nat
 type family (m :: Nat) ^ (n :: Nat) :: Nat
 type family (m :: Nat)  (n :: Nat) :: Nat
 type family Div (m :: Nat) (n :: Nat) :: Nat
 type family Mod (m :: Nat) (n :: Nat) :: Nat
 type family Log2 (m :: Nat) :: Nat
 type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol
 type family CmpNat (m :: Natural) (n :: Natural) :: Ordering
 type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
 type family CmpChar (a :: Char) (b :: Char) :: Ordering
 type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol
 type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)
 type family CharToNat (c :: Char) :: Nat
 type family NatToChar (n :: Nat) :: Char
 type family TypeError (a :: ErrorMessage) :: b where ...
 data ErrorMessage
 = Text Symbol
  forall t. ShowType t
  ErrorMessage :<>: ErrorMessage
  ErrorMessage :$$: ErrorMessage
Kinds
Natural number
Invariant: numbers <= 0xffffffffffffffff use the NS
constructor
Instances
A type synonym for Natural
.
Prevously, this was an opaque data type, but it was changed to a type synonym.
Since: base4.15.0.0
(Kind) This is the kind of typelevel symbols. Declared here because class IP needs it
Linking type and value level
class KnownNat (n :: Nat) Source #
This class gives the integer associated with a typelevel natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base4.7.0.0
natSing
class KnownSymbol (n :: Symbol) Source #
This class gives the string associated with a typelevel symbol. There are instances of the class for every concrete literal: "hello", etc.
Since: base4.7.0.0
symbolSing
symbolVal :: forall n proxy. KnownSymbol n => proxy n > String Source #
Since: base4.7.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n > String Source #
Since: base4.8.0.0
This type represents unknown typelevel natural numbers.
Since: base4.10.0.0
Instances
Read SomeNat #  Since: base4.7.0.0 
Show SomeNat #  Since: base4.7.0.0 
Eq SomeNat #  Since: base4.7.0.0 
Ord SomeNat #  Since: base4.7.0.0 
data SomeSymbol Source #
This type represents unknown typelevel symbols.
forall n.KnownSymbol n => SomeSymbol (Proxy n)  Since: base4.7.0.0 
Instances
Read SomeSymbol #  Since: base4.7.0.0 
Defined in GHC.TypeLits  
Show SomeSymbol #  Since: base4.7.0.0 
Defined in GHC.TypeLits  
Eq SomeSymbol #  Since: base4.7.0.0 
Defined in GHC.TypeLits (==) :: SomeSymbol > SomeSymbol > Bool Source # (/=) :: SomeSymbol > SomeSymbol > Bool Source #  
Ord SomeSymbol #  Since: base4.7.0.0 
Defined in GHC.TypeLits compare :: SomeSymbol > SomeSymbol > Ordering Source # (<) :: SomeSymbol > SomeSymbol > Bool Source # (<=) :: SomeSymbol > SomeSymbol > Bool Source # (>) :: SomeSymbol > SomeSymbol > Bool Source # (>=) :: SomeSymbol > SomeSymbol > Bool Source # max :: SomeSymbol > SomeSymbol > SomeSymbol Source # min :: SomeSymbol > SomeSymbol > SomeSymbol Source # 
Instances
Read SomeChar #  
Show SomeChar #  
Eq SomeChar #  
Ord SomeChar #  
Defined in GHC.TypeLits 
someNatVal :: Integer > Maybe SomeNat Source #
Convert an integer into an unknown typelevel natural.
Since: base4.7.0.0
someSymbolVal :: String > SomeSymbol Source #
Convert a string into an unknown typelevel symbol.
Since: base4.7.0.0
someCharVal :: Char > SomeChar Source #
Convert a character into an unknown typelevel char.
Since: base4.16.0.0
sameNat :: (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Maybe (a :~: b) Source #
We either get evidence that this function was instantiated with the
same typelevel numbers, or Nothing
.
Since: base4.7.0.0
sameSymbol :: (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Maybe (a :~: b) Source #
We either get evidence that this function was instantiated with the
same typelevel symbols, or Nothing
.
Since: base4.7.0.0
sameChar :: (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > Maybe (a :~: b) Source #
We either get evidence that this function was instantiated with the
same typelevel characters, or Nothing
.
Since: base4.16.0.0
data OrderingI a b where Source #
Ordering data type for type literals that provides proof of their ordering.
Since: base4.16.0.0
LTI :: Compare a b ~ 'LT => OrderingI a b  
EQI :: Compare a a ~ 'EQ => OrderingI a a  
GTI :: Compare a b ~ 'GT => OrderingI a b 
cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > OrderingI a b Source #
Like sameNat
, but if the numbers aren't equal, this additionally
provides proof of LT or GT.
Since: base4.16.0.0
cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > OrderingI a b Source #
Like sameSymbol
, but if the symbols aren't equal, this additionally
provides proof of LT or GT.
Since: base4.16.0.0
cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > OrderingI a b Source #
Like sameChar
, but if the Chars aren't equal, this additionally
provides proof of LT or GT.
Since: base4.16.0.0
Functions on type literals
type (<=) x y = Assert (x <=? y) (LeErrMsg x y) infix 4 Source #
Comparison (<=) of comparable types, as a constraint.
Since: base4.16.0.0
type (<=?) m n = OrdCond (Compare m n) 'True 'True 'False infix 4 Source #
Comparison (<=) of comparable types, as a function.
Since: base4.16.0.0
type family (m :: Nat) + (n :: Nat) :: Nat infixl 6 Source #
Addition of typelevel naturals.
Since: base4.7.0.0
type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Source #
Multiplication of typelevel naturals.
Since: base4.7.0.0
type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 Source #
Exponentiation of typelevel naturals.
Since: base4.7.0.0
type family (m :: Nat)  (n :: Nat) :: Nat infixl 6 Source #
Subtraction of typelevel naturals.
Since: base4.7.0.0
type family Div (m :: Nat) (n :: Nat) :: Nat infixl 7 Source #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: base4.11.0.0
type family Mod (m :: Nat) (n :: Nat) :: Nat infixl 7 Source #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: base4.11.0.0
type family Log2 (m :: Nat) :: Nat Source #
Log base 2 (round down) of natural numbers.
Log 0
is undefined (i.e., it cannot be reduced).
Since: base4.11.0.0
type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol Source #
Concatenation of typelevel symbols.
Since: base4.10.0.0
type family CmpNat (m :: Natural) (n :: Natural) :: Ordering Source #
Comparison of typelevel naturals, as a function.
Since: base4.7.0.0
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering Source #
Comparison of typelevel symbols, as a function.
Since: base4.7.0.0
type family CmpChar (a :: Char) (b :: Char) :: Ordering Source #
Comparison of typelevel characters.
Since: base4.16.0.0
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol Source #
Extending a typelevel symbol with a typelevel character
Since: base4.16.0.0
type family CharToNat (c :: Char) :: Nat Source #
Convert a character to its Unicode code point (cf. ord
)
Since: base4.16.0.0
type family NatToChar (n :: Nat) :: Char Source #
Convert a Unicode code point to a character (cf. chr
)
Since: base4.16.0.0
Userdefined type errors
type family TypeError (a :: ErrorMessage) :: b where ... Source #
The typelevel 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 nonexistent 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 righthand side of a typelevel 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: base4.9.0.0
data ErrorMessage Source #
A description of a custom type error.
Text Symbol  Show the text as is. 
forall t. ShowType t  Pretty print the type.

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. 