| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
GHC.TypeLits
Description
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 type-level 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 type-level strings to support user
defined type errors.
For now, this module is the API for working with type-level 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 type-level data will be defined in a separate library.
Since: base-4.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: base-4.15.0.0
(Kind) This is the kind of type-level 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 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
class KnownSymbol (n :: Symbol) Source #
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 proxy. KnownSymbol n => proxy n -> String Source #
Since: base-4.7.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String Source #
Since: base-4.8.0.0
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
Instances
| Read SomeNat Source # | Since: base-4.7.0.0 |
| Show SomeNat Source # | Since: base-4.7.0.0 |
| Eq SomeNat Source # | Since: base-4.7.0.0 |
| Ord SomeNat Source # | Since: base-4.7.0.0 |
data SomeSymbol Source #
This type represents unknown type-level symbols.
Constructors
| forall n.KnownSymbol n => SomeSymbol (Proxy n) | Since: base-4.7.0.0 |
Instances
| Read SomeSymbol Source # | Since: base-4.7.0.0 |
Defined in GHC.TypeLits | |
| Show SomeSymbol Source # | Since: base-4.7.0.0 |
Defined in GHC.TypeLits | |
| Eq SomeSymbol Source # | Since: base-4.7.0.0 |
Defined in GHC.TypeLits Methods (==) :: SomeSymbol -> SomeSymbol -> Bool Source # (/=) :: SomeSymbol -> SomeSymbol -> Bool Source # | |
| Ord SomeSymbol Source # | Since: base-4.7.0.0 |
Defined in GHC.TypeLits Methods 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.TypeLits | |
someNatVal :: Integer -> Maybe SomeNat Source #
Convert an integer into an unknown type-level natural.
Since: base-4.7.0.0
someSymbolVal :: String -> SomeSymbol Source #
Convert a string into an unknown type-level symbol.
Since: base-4.7.0.0
someCharVal :: Char -> SomeChar Source #
Convert a character into an unknown type-level char.
Since: base-4.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 type-level numbers, or Nothing.
Since: base-4.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 type-level symbols, or Nothing.
Since: base-4.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 type-level characters, or Nothing.
Since: base-4.16.0.0
data OrderingI a b where Source #
Ordering data type for type literals that provides proof of their ordering.
Since: base-4.16.0.0
Constructors
| 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: base-4.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: base-4.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: base-4.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: base-4.16.0.0
type (<=?) m n = OrdCond (Compare m n) 'True 'True 'False infix 4 Source #
Comparison (<=) of comparable types, as a function.
Since: base-4.16.0.0
type family (m :: Nat) + (n :: Nat) :: Nat infixl 6 Source #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Source #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 Source #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat infixl 6 Source #
Subtraction of type-level naturals.
Since: base-4.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: base-4.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: base-4.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: base-4.11.0.0
type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol Source #
Concatenation of type-level symbols.
Since: base-4.10.0.0
type family CmpNat (m :: Natural) (n :: Natural) :: Ordering Source #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering Source #
Comparison of type-level symbols, as a function.
Since: base-4.7.0.0
type family CmpChar (a :: Char) (b :: Char) :: Ordering Source #
Comparison of type-level characters.
Since: base-4.16.0.0
type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol Source #
Extending a type-level symbol with a type-level character
Since: base-4.16.0.0
type family CharToNat (c :: Char) :: Nat Source #
Convert a character to its Unicode code point (cf. ord)
Since: base-4.16.0.0
type family NatToChar (n :: Nat) :: Char Source #
Convert a Unicode code point to a character (cf. chr)
Since: base-4.16.0.0
User-defined type errors
type family TypeError (a :: ErrorMessage) :: b where ... Source #
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 Source #
A description of a custom type error.
Constructors
| 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. |