GHC.TypeLits (original) (raw)
data Nat #
(Kind) This is the kind of type-level natural numbers.
data Symbol #
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
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
This type represents unknown type-level natural numbers.
Since: 4.10.0.0
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](GHC-TypeLits.html#t:CmpNat "GHC.TypeLits"), 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 infixl 7 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 infixl 7 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 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](Text-Show.html#t:Show "Text.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