Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
GHC.TypeLits
Description
This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface for working with type-level naturals should be defined in a separate library.
Since: 4.6.0.0
Synopsis
- data Nat :: *
- 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
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- data SomeSymbol = KnownSymbol n => SomeSymbol (Proxy n)
- someNatVal :: Integer -> Maybe SomeNat
- someSymbolVal :: String -> SomeSymbol
- sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- type (<=) x y = (x <=? y) ~ True
- type family (m :: Nat) <=? (n :: Nat) :: Bool
- 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 :: Nat) (n :: Nat) :: Ordering
- type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
- type family TypeError (a :: ErrorMessage) :: b where ...
- data ErrorMessage
Kinds
(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: 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: 4.7.0.0
Minimal complete definition
symbolSing
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String Source #
Since: 4.7.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String Source #
Since: 4.8.0.0
This type represents unknown type-level natural numbers.
Since: 4.10.0.0
Instances
Eq SomeNat # | Since: 4.7.0.0 |
Ord SomeNat # | Since: 4.7.0.0 |
Read SomeNat # | Since: 4.7.0.0 |
Show SomeNat # | Since: 4.7.0.0 |
data SomeSymbol Source #
This type represents unknown type-level symbols.
Constructors
KnownSymbol n => SomeSymbol (Proxy n) | Since: 4.7.0.0 |
Instances
Eq SomeSymbol # | Since: 4.7.0.0 |
Methods (==) :: SomeSymbol -> SomeSymbol -> Bool Source # (/=) :: SomeSymbol -> SomeSymbol -> Bool Source # | |
Ord SomeSymbol # | Since: 4.7.0.0 |
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 # | |
Read SomeSymbol # | Since: 4.7.0.0 |
Show SomeSymbol # | Since: 4.7.0.0 |
someNatVal :: Integer -> Maybe SomeNat Source #
Convert an integer into an unknown type-level natural.
Since: 4.7.0.0
someSymbolVal :: String -> SomeSymbol Source #
Convert a string into an unknown type-level symbol.
Since: 4.7.0.0
sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source #
We either get evidence that this function was instantiated with the
same type-level numbers, or Nothing
.
Since: 4.7.0.0
sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source #
We either get evidence that this function was instantiated with the
same type-level symbols, or Nothing
.
Since: 4.7.0.0
Functions on type literals
type (<=) x y = (x <=? y) ~ True infix 4 Source #
Comparison of type-level naturals, as a constraint.
Since: 4.7.0.0
type family (m :: Nat) <=? (n :: Nat) :: Bool infix 4 Source #
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat
, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.
type family (m :: Nat) + (n :: Nat) :: Nat infixl 6 Source #
Addition of type-level naturals.
Since: 4.7.0.0
type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Source #
Multiplication of type-level naturals.
Since: 4.7.0.0
type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 Source #
Exponentiation of type-level naturals.
Since: 4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat infixl 6 Source #
Subtraction of type-level naturals.
Since: 4.7.0.0
type family Div (m :: Nat) (n :: Nat) :: Nat Source #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type family Mod (m :: Nat) (n :: Nat) :: Nat Source #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: 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: 4.11.0.0
type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol Source #
Concatenation of type-level symbols.
Since: 4.10.0.0
type family CmpNat (m :: Nat) (n :: Nat) :: Ordering Source #
Comparison of type-level naturals, as a function.
Since: 4.7.0.0
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering Source #
Comparison of type-level symbols, as a function.
Since: 4.7.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: 4.9.0.0
data ErrorMessage Source #
A description of a custom type error.
Constructors
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. |