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) where
 natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n > Integer
 natVal' :: forall (n :: Nat). KnownNat n => Proxy# n > Integer
 class KnownSymbol (n :: Symbol) where
 symbolSing :: SSymbol n
 symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n > String
 symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n > String
 class KnownChar (n :: Char) where
 charVal :: forall (n :: Char) proxy. KnownChar n => proxy n > Char
 charVal' :: forall (n :: Char). KnownChar n => Proxy# n > Char
 data SomeNat = KnownNat n => SomeNat (Proxy n)
 data SomeSymbol = KnownSymbol n => SomeSymbol (Proxy n)
 data SomeChar = KnownChar n => SomeChar (Proxy n)
 someNatVal :: Integer > Maybe SomeNat
 someSymbolVal :: String > SomeSymbol
 someCharVal :: Char > SomeChar
 sameNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Maybe (a :~: b)
 sameSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Maybe (a :~: b)
 sameChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > Maybe (a :~: b)
 decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Either ((a :~: b) > Void) (a :~: b)
 decideSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Either ((a :~: b) > Void) (a :~: b)
 decideChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > Either ((a :~: b) > Void) (a :~: b)
 data OrderingI (a :: k) (b :: k) where
 cmpNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > OrderingI a b
 cmpSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > OrderingI a b
 cmpChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > OrderingI a b
 data SNat (n :: Nat) where
 pattern UnsafeSNat :: Natural > SNat n
 data SSymbol (s :: Symbol) where
 pattern UnsafeSSymbol :: String > SSymbol s
 data SChar (s :: Char) where
 pattern UnsafeSChar :: Char > SChar c
 pattern SNat :: () => KnownNat n => SNat n
 pattern SSymbol :: () => KnownSymbol s => SSymbol s
 pattern SChar :: () => KnownChar c => SChar c
 fromSNat :: forall (n :: Nat). SNat n > Integer
 fromSSymbol :: forall (s :: Symbol). SSymbol s > String
 fromSChar :: forall (c :: Char). SChar c > Char
 withSomeSNat :: Integer > (forall (n :: Nat). Maybe (SNat n) > r) > r
 withSomeSSymbol :: String > (forall (s :: Symbol). SSymbol s > r) > r
 withSomeSChar :: Char > (forall (c :: Char). SChar c > r) > r
 withKnownNat :: forall (n :: Nat) r. SNat n > (KnownNat n => r) > r
 withKnownSymbol :: forall (s :: Symbol) r. SSymbol s > (KnownSymbol s => r) > r
 withKnownChar :: forall (c :: Char) r. SChar c > (KnownChar c => r) > r
 unsafeWithSNatCo :: ((forall (n :: Nat). Coercible (SNat n) Natural) => r) > r
 unsafeWithSSymbolCo :: ((forall (s :: Symbol). Coercible (SSymbol s) String) => r) > r
 unsafeWithSCharCo :: ((forall (c :: Char). Coercible (SChar c) Char) => r) > r
 type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint)
 type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False
 type family (a :: Natural) + (b :: Natural) :: Natural where ...
 type family (a :: Natural) * (b :: Natural) :: Natural where ...
 type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
 type family (a :: Natural)  (b :: Natural) :: Natural where ...
 type family Div (a :: Natural) (b :: Natural) :: Natural where ...
 type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
 type family Log2 (a :: Natural) :: Natural where ...
 type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ...
 type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ...
 type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ...
 type family CmpChar (a :: Char) (b :: Char) :: Ordering where ...
 type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ...
 type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) where ...
 type family CharToNat (a :: Char) :: Natural where ...
 type family NatToChar (a :: Natural) :: Char where ...
 type family TypeError (a :: ErrorMessage) :: b where ...
 data ErrorMessage
Kinds
Natural number
Invariant: numbers <= 0xffffffffffffffff use the NS
constructor
Instances
A type synonym for Natural
.
Previously, this was an opaque data type, but it was changed to a type synonym.
Since: base4.16.0.0
(Kind) This is the kind of typelevel symbols.
Instances
TestCoercion SSymbol Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeLits  
TestEquality SSymbol Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeLits  
type Compare (a :: Symbol) (b :: Symbol) Source #  
Defined in GHC.Internal.Data.Type.Ord 
Linking type and value level
class KnownNat (n :: Nat) where 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
class KnownSymbol (n :: Symbol) where 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 :: SSymbol n Source #
symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n > String Source #
Since: base4.7.0.0
symbolVal' :: forall (n :: Symbol). 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 Source #  Since: base4.7.0.0 
Show SomeNat Source #  Since: base4.7.0.0 
Eq SomeNat Source #  Since: base4.7.0.0 
Ord SomeNat Source #  Since: base4.7.0.0 
data SomeSymbol Source #
This type represents unknown typelevel symbols.
KnownSymbol n => SomeSymbol (Proxy n)  Since: base4.7.0.0 
Instances
Read SomeSymbol Source #  Since: base4.7.0.0 
Defined in GHC.Internal.TypeLits  
Show SomeSymbol Source #  Since: base4.7.0.0 
Defined in GHC.Internal.TypeLits  
Eq SomeSymbol Source #  Since: base4.7.0.0 
Defined in GHC.Internal.TypeLits (==) :: SomeSymbol > SomeSymbol > Bool Source # (/=) :: SomeSymbol > SomeSymbol > Bool Source #  
Ord SomeSymbol Source #  Since: base4.7.0.0 
Defined in GHC.Internal.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 Source #  
Show SomeChar Source #  
Eq SomeChar Source #  
Ord SomeChar Source #  
Defined in GHC.Internal.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 :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (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 :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (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 :: forall (a :: Char) (b :: Char) proxy1 proxy2. (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
decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a > proxy2 b > Either ((a :~: b) > Void) (a :~: b) Source #
We either get evidence that this function was instantiated with the same typelevel numbers, or that the typelevel numbers are distinct.
Since: base4.19.0.0
decideSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a > proxy2 b > Either ((a :~: b) > Void) (a :~: b) Source #
We either get evidence that this function was instantiated with the same typelevel symbols, or that the typelevel symbols are distinct.
Since: base4.19.0.0
decideChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a > proxy2 b > Either ((a :~: b) > Void) (a :~: b) Source #
We either get evidence that this function was instantiated with the same typelevel characters, or that the typelevel characters are distinct.
Since: base4.19.0.0
data OrderingI (a :: k) (b :: k) where Source #
Ordering data type for type literals that provides proof of their ordering.
Since: base4.16.0.0
LTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'LT => OrderingI a b  
EQI :: forall {k} (a :: k). Compare a a ~ 'EQ => OrderingI a a  
GTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'GT => OrderingI a b 
cmpNat :: forall (a :: Nat) (b :: Nat) 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 :: Symbol) (b :: Symbol) 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 :: Char) (b :: Char) 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
Singleton values
data SNat (n :: Nat) where Source #
A valuelevel witness for a typelevel natural number. This is commonly
referred to as a singleton type, as for each n
, there is a single value
that inhabits the type
(aside from bottom).SNat
n
The definition of SNat
is intentionally left abstract. To obtain an SNat
value, use one of the following:
 The
natSing
method ofKnownNat
.  The
SNat
pattern synonym.  The
withSomeSNat
function, which creates anSNat
from aNatural
number.
Since: base4.18.0.0
pattern UnsafeSNat :: Natural > SNat n  A pattern that can be used to manipulate the
When using this pattern to construct an 
Instances
TestCoercion SNat Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeNats  
TestEquality SNat Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeNats  
Show (SNat n) Source #  Since: base4.18.0.0 
Eq (SNat n) Source #  Since: base4.19.0.0 
Ord (SNat n) Source #  Since: base4.19.0.0 
Defined in GHC.Internal.TypeNats 
data SSymbol (s :: Symbol) where Source #
A valuelevel witness for a typelevel symbol. This is commonly referred
to as a singleton type, as for each s
, there is a single value that
inhabits the type
(aside from bottom).SSymbol
s
The definition of SSymbol
is intentionally left abstract. To obtain an
SSymbol
value, use one of the following:
 The
symbolSing
method ofKnownSymbol
.  The
SSymbol
pattern synonym.  The
withSomeSSymbol
function, which creates anSSymbol
from aString
.
Since: base4.18.0.0
pattern UnsafeSSymbol :: String > SSymbol s  A pattern that can be used to manipulate the
When using this pattern to construct an 
Instances
TestCoercion SSymbol Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeLits  
TestEquality SSymbol Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeLits  
Show (SSymbol s) Source #  Since: base4.18.0.0 
Eq (SSymbol s) Source #  Since: base4.19.0.0 
Ord (SSymbol s) Source #  Since: base4.19.0.0 
Defined in GHC.Internal.TypeLits 
data SChar (s :: Char) where Source #
A valuelevel witness for a typelevel character. This is commonly referred
to as a singleton type, as for each c
, there is a single value that
inhabits the type
(aside from bottom).SChar
c
The definition of SChar
is intentionally left abstract. To obtain an
SChar
value, use one of the following:
 The
charSing
method ofKnownChar
.  The
SChar
pattern synonym.  The
withSomeSChar
function, which creates anSChar
from aChar
.
Since: base4.18.0.0
pattern UnsafeSChar :: Char > SChar c  A pattern that can be used to manipulate the
When using this pattern to construct an 
Instances
TestCoercion SChar Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeLits  
TestEquality SChar Source #  Since: base4.18.0.0 
Defined in GHC.Internal.TypeLits  
Show (SChar c) Source #  Since: base4.18.0.0 
Eq (SChar c) Source #  Since: base4.19.0.0 
Ord (SChar c) Source #  Since: base4.19.0.0 
pattern SNat :: () => KnownNat n => SNat n Source #
A explicitly bidirectional pattern synonym relating an SNat
to a
KnownNat
constraint.
As an expression: Constructs an explicit
value from an
implicit SNat
n
constraint:KnownNat
n
SNat @n ::KnownNat
n =>SNat
n
As a pattern: Matches on an explicit
value bringing
an implicit SNat
n
constraint into scope:KnownNat
n
f :: SNat
n > ..
f SNat = { KnownNat n in scope }
Since: base4.18.0.0
pattern SSymbol :: () => KnownSymbol s => SSymbol s Source #
A explicitly bidirectional pattern synonym relating an SSymbol
to a
KnownSymbol
constraint.
As an expression: Constructs an explicit
value from an
implicit SSymbol
s
constraint:KnownSymbol
s
SSymbol @s ::KnownSymbol
s =>SSymbol
s
As a pattern: Matches on an explicit
value bringing
an implicit SSymbol
s
constraint into scope:KnownSymbol
s
f :: SSymbol
s > ..
f SSymbol = { KnownSymbol s in scope }
Since: base4.18.0.0
pattern SChar :: () => KnownChar c => SChar c Source #
A explicitly bidirectional pattern synonym relating an SChar
to a
KnownChar
constraint.
As an expression: Constructs an explicit
value from an
implicit SChar
c
constraint:KnownChar
c
SChar @c ::KnownChar
c =>SChar
c
As a pattern: Matches on an explicit
value bringing
an implicit SChar
c
constraint into scope:KnownChar
c
f :: SChar
c > ..
f SChar = { KnownChar c in scope }
Since: base4.18.0.0
fromSNat :: forall (n :: Nat). SNat n > Integer Source #
Return the Integer
corresponding to n
in an
value.
The returned SNat
nInteger
is always nonnegative.
For a version of this function that returns a Natural
instead of an
Integer
, see fromSNat
in GHC.TypeNats.
Since: base4.18.0.0
fromSSymbol :: forall (s :: Symbol). SSymbol s > String Source #
Return the String corresponding to s
in an
value.SSymbol
s
Since: base4.18.0.0
withSomeSNat :: Integer > (forall (n :: Nat). Maybe (SNat n) > r) > r Source #
Attempt to convert an Integer
into an
value, where SNat
nn
is a
fresh typelevel natural number. If the Integer
argument is nonnegative,
invoke the continuation with Just sn
, where sn
is the
value.
If the SNat
nInteger
argument is negative, invoke the continuation with
Nothing
.
For a version of this function where the continuation uses 'SNat
n
instead of
Maybe
(SNat
n)@, see withSomeSNat
in GHC.TypeNats.
Since: base4.18.0.0
withKnownSymbol :: forall (s :: Symbol) r. SSymbol s > (KnownSymbol s => r) > r Source #
Convert an explicit
value into an implicit SSymbol
s
constraint.KnownSymbol
s
Since: base4.18.0.0
unsafeWithSNatCo :: ((forall (n :: Nat). Coercible (SNat n) Natural) => r) > r Source #
unsafeWithSNatCo
allows uses of coerce
in its argument to see the
real representation of SNat n
, without undermining the typesafety of
coerce
elsewhere in the module.
See also the documentation for UnsafeSNat
.
unsafeWithSSymbolCo :: ((forall (s :: Symbol). Coercible (SSymbol s) String) => r) > r Source #
unsafeWithSSymbolCo
allows uses of coerce
in its argument to see the
real representation of SSymbol s
, without undermining the typesafety of
coerce
elsewhere in the module.
See also the documentation for UnsafeSSymbol
.
unsafeWithSCharCo :: ((forall (c :: Char). Coercible (SChar c) Char) => r) > r Source #
unsafeWithSCharCo
allows uses of coerce
in its argument to see the
real representation of SChar c
, without undermining the typesafety of
coerce
elsewhere in the module.
See also the documentation for UnsafeSChar
.
Functions on type literals
type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 Source #
Comparison (<=) of comparable types, as a constraint.
Since: base4.16.0.0
type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 Source #
Comparison (<=) of comparable types, as a function.
Since: base4.16.0.0
type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 Source #
Addition of typelevel naturals.
Since: base4.7.0.0
type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 Source #
Multiplication of typelevel naturals.
Since: base4.7.0.0
type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 Source #
Exponentiation of typelevel naturals.
Since: base4.7.0.0
type family (a :: Natural)  (b :: Natural) :: Natural where ... infixl 6 Source #
Subtraction of typelevel naturals.
Since: base4.7.0.0
type family Div (a :: Natural) (b :: Natural) :: Natural where ... 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 (a :: Natural) (b :: Natural) :: Natural where ... 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 (a :: Natural) :: Natural where ... 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 (a :: Symbol) (b :: Symbol) :: Symbol where ... Source #
Concatenation of typelevel symbols.
Since: base4.10.0.0
type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Source #
Comparison of typelevel naturals, as a function.
Since: base4.7.0.0
type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... Source #
Comparison of typelevel symbols, as a function.
Since: base4.7.0.0
type family CmpChar (a :: Char) (b :: Char) :: Ordering where ... Source #
Comparison of typelevel characters.
Since: base4.16.0.0
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ... Source #
Extending a typelevel symbol with a typelevel character
Since: base4.16.0.0
type family CharToNat (a :: Char) :: Natural where ... Source #
Convert a character to its Unicode code point (cf. ord
)
Since: base4.16.0.0
type family NatToChar (a :: Natural) :: Char where ... 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. 
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. 