GHC.TypeLits

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) and strings (the Symbol) 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

Kinds

data Nat

(Kind) This is the kind of type-level natural numbers.

Instances

KnownNat n => HasResolution (n :: Nat)

For example, Fixed 1000 will give you a Fixed with a resolution of 1000.

Defined in Data.Fixed

Methods

resolution :: p n -> Integer

data Symbol

(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)

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

natVal :: forall n proxy. KnownNat n => proxy n -> Integer

Since: base-4.7.0.0

natVal' :: forall n. KnownNat n => Proxy# n -> Integer

Since: base-4.8.0.0

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

data SomeNat

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

forall n.KnownNat n => SomeNat (Proxy n)

Instances

Eq SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool

(/=) :: SomeNat -> SomeNat -> Bool

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering

(<) :: SomeNat -> SomeNat -> Bool

(<=) :: SomeNat -> SomeNat -> Bool

(>) :: SomeNat -> SomeNat -> Bool

(>=) :: SomeNat -> SomeNat -> Bool

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

Read SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

data SomeSymbol

This type represents unknown type-level symbols.

Constructors

forall n.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

(/=) :: SomeSymbol -> SomeSymbol -> Bool

Ord SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

compare :: SomeSymbol -> SomeSymbol -> Ordering

(<) :: SomeSymbol -> SomeSymbol -> Bool

(<=) :: SomeSymbol -> SomeSymbol -> Bool

(>) :: SomeSymbol -> SomeSymbol -> Bool

(>=) :: SomeSymbol -> SomeSymbol -> Bool

max :: SomeSymbol -> SomeSymbol -> SomeSymbol

min :: SomeSymbol -> SomeSymbol -> SomeSymbol

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.

forall t. ShowType t

Pretty print the type. ShowType :: k -> ErrorMessage

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.