| 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: base-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
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) #
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 #
Since: base-4.7.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String #
Since: base-4.8.0.0
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
Instances
| Eq SomeNat # | Since: base-4.7.0.0 |
| Ord SomeNat # | Since: base-4.7.0.0 |
| Read SomeNat # | Since: base-4.7.0.0 |
| Show SomeNat # | Since: base-4.7.0.0 |
data SomeSymbol #
This type represents unknown type-level symbols.
Constructors
| KnownSymbol n => SomeSymbol (Proxy n) | Since: base-4.7.0.0 |
Instances
| Eq SomeSymbol # | Since: base-4.7.0.0 |
Defined in GHC.TypeLits Methods (==) :: SomeSymbol -> SomeSymbol -> Bool Source # (/=) :: SomeSymbol -> SomeSymbol -> Bool Source # | |
| Ord SomeSymbol # | 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 # | |
| 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 :: Integer -> Maybe SomeNat #
Convert an integer into an unknown type-level natural.
Since: base-4.7.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 (<=) x y = (x <=? y) ~ True infix 4 #
Comparison of type-level naturals, as a constraint.
Since: base-4.7.0.0
type family (m :: Nat) <=? (n :: Nat) :: Bool infix 4 #
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 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (m :: Nat) - (n :: Nat) :: Nat infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family Div (m :: Nat) (n :: Nat) :: Nat 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 (m :: Nat) (n :: Nat) :: Nat 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 (m :: Nat) :: Nat #
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 #
Concatenation of type-level symbols.
Since: base-4.10.0.0
type family CmpNat (m :: Nat) (n :: Nat) :: Ordering #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering #
Comparison of type-level symbols, as a function.
Since: base-4.7.0.0
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 #
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. |