base-4.17.0.0: Basic libraries
Safe HaskellTrustworthy
LanguageHaskell2010

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

Kinds

data Natural Source #

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Instances

Instances details
Data Natural Source #

Since: base-4.8.0.0

Instance details

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Natural -> c Natural Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Natural Source #

toConstr :: Natural -> Constr Source #

dataTypeOf :: Natural -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Natural) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Natural) Source #

gmapT :: (forall b. Data b => b -> b) -> Natural -> Natural Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Natural -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Natural -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Natural -> m Natural Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural Source #

Bits Natural Source #

Since: base-4.8.0

Instance details

Defined in GHC.Bits

Enum Natural Source #

Since: base-4.8.0.0

Instance details

Defined in GHC.Enum

Ix Natural Source #

Since: base-4.8.0.0

Instance details

Defined in GHC.Ix

Num Natural Source #

Note that Natural's Num instance isn't a ring: no element but 0 has an additive inverse. It is a semiring though.

Since: base-4.8.0.0

Instance details

Defined in GHC.Num

Read Natural Source #

Since: base-4.8.0.0

Instance details

Defined in GHC.Read

Integral Natural Source #

Since: base-4.8.0.0

Instance details

Defined in GHC.Real

Real Natural Source #

Since: base-4.8.0.0

Instance details

Defined in GHC.Real

Show Natural Source #

Since: base-4.8.0.0

Instance details

Defined in GHC.Show

PrintfArg Natural Source #

Since: base-4.8.0.0

Instance details

Defined in Text.Printf

Eq Natural 
Instance details

Defined in GHC.Num.Natural

Ord Natural 
Instance details

Defined in GHC.Num.Natural

KnownNat n => HasResolution (n :: Nat) Source #

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

Instance details

Defined in Data.Fixed

Methods

resolution :: p n -> Integer Source #

TestCoercion SNat Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeNats

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b) Source #

TestEquality SNat Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) Source #

type Compare (a :: Natural) (b :: Natural) Source # 
Instance details

Defined in Data.Type.Ord

type Compare (a :: Natural) (b :: Natural) = CmpNat a b

type Nat = Natural Source #

A type synonym for Natural.

Prevously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

data Symbol Source #

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

Instances

Instances details
TestCoercion SSymbol Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

Methods

testCoercion :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (Coercion a b) Source #

TestEquality SSymbol Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b) Source #

type Compare (a :: Symbol) (b :: Symbol) Source # 
Instance details

Defined in Data.Type.Ord

type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b

Linking type and value level

class KnownNat (n :: Nat) where 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

Methods

natSing :: SNat n Source #

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

Since: base-4.7.0.0

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

Since: base-4.8.0.0

class KnownSymbol (n :: Symbol) where 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

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

class KnownChar (n :: Char) where Source #

Since: base-4.16.0.0

Methods

charSing :: SChar n Source #

charVal :: forall n proxy. KnownChar n => proxy n -> Char Source #

charVal' :: forall n. KnownChar n => Proxy# n -> Char Source #

data SomeNat Source #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

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

Instances

Instances details
Read SomeNat Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Show SomeNat Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Eq SomeNat Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Ord SomeNat Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

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

Instances details
Read SomeSymbol Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Show SomeSymbol Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Eq SomeSymbol Source #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Ord SomeSymbol Source #

Since: base-4.7.0.0

Instance details

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 :: forall a b proxy1 proxy2. (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 :: forall a b proxy1 proxy2. (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 :: forall a b proxy1 proxy2. (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 

Instances

Instances details
Show (OrderingI a b) Source # 
Instance details

Defined in Data.Type.Ord

Eq (OrderingI a b) Source # 
Instance details

Defined in Data.Type.Ord

Methods

(==) :: OrderingI a b -> OrderingI a b -> Bool Source #

(/=) :: OrderingI a b -> OrderingI a b -> Bool Source #

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

Singleton values

data SNat (n :: Nat) Source #

A value-level witness for a type-level natural number. This is commonly referred to as a singleton type, as for each n, there is a single value that inhabits the type SNat n (aside from bottom).

The definition of SNat is intentionally left abstract. To obtain an SNat value, use one of the following:

  1. The natSing method of KnownNat.
  2. The SNat pattern synonym.
  3. The withSomeSNat function, which creates an SNat from a Natural number.

Since: base-4.18.0.0

Instances

Instances details
TestCoercion SNat Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeNats

Methods

testCoercion :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (Coercion a b) Source #

TestEquality SNat Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeNats

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b) Source #

Show (SNat n) Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SNat n -> ShowS Source #

show :: SNat n -> String Source #

showList :: [SNat n] -> ShowS Source #

data SSymbol (s :: Symbol) Source #

A value-level witness for a type-level symbol. This is commonly referred to as a singleton type, as for each s, there is a single value that inhabits the type SSymbol s (aside from bottom).

The definition of SSymbol is intentionally left abstract. To obtain an SSymbol value, use one of the following:

  1. The symbolSing method of KnownSymbol.
  2. The SSymbol pattern synonym.
  3. The withSomeSSymbol function, which creates an SSymbol from a String.

Since: base-4.18.0.0

Instances

Instances details
TestCoercion SSymbol Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

Methods

testCoercion :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (Coercion a b) Source #

TestEquality SSymbol Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: k) (b :: k). SSymbol a -> SSymbol b -> Maybe (a :~: b) Source #

Show (SSymbol s) Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

data SChar (s :: Char) Source #

A value-level witness for a type-level character. This is commonly referred to as a singleton type, as for each c, there is a single value that inhabits the type SChar c (aside from bottom).

The definition of SChar is intentionally left abstract. To obtain an SChar value, use one of the following:

  1. The charSing method of KnownChar.
  2. The SChar pattern synonym.
  3. The withSomeSChar function, which creates an SChar from a Char.

Since: base-4.18.0.0

Instances

Instances details
TestCoercion SChar Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

Methods

testCoercion :: forall (a :: k) (b :: k). SChar a -> SChar b -> Maybe (Coercion a b) Source #

TestEquality SChar Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

Methods

testEquality :: forall (a :: k) (b :: k). SChar a -> SChar b -> Maybe (a :~: b) Source #

Show (SChar c) Source #

Since: base-4.18.0.0

Instance details

Defined in GHC.TypeLits

pattern SNat :: forall n. () => KnownNat n => SNat n Source #

A explicitly bidirectional pattern synonym relating an SNat to a KnownNat constraint.

As an expression: Constructs an explicit SNat n value from an implicit KnownNat n constraint:

SNat @n :: KnownNat n => SNat n

As a pattern: Matches on an explicit SNat n value bringing an implicit KnownNat n constraint into scope:

f :: SNat n -> ..
f SNat = {- SNat n in scope -}

Since: base-4.18.0.0

pattern SSymbol :: forall s. () => KnownSymbol s => SSymbol s Source #

A explicitly bidirectional pattern synonym relating an SSymbol to a KnownSymbol constraint.

As an expression: Constructs an explicit SSymbol s value from an implicit KnownSymbol s constraint:

SSymbol @s :: KnownSymbol s => SSymbol s

As a pattern: Matches on an explicit SSymbol s value bringing an implicit KnownSymbol s constraint into scope:

f :: SSymbol s -> ..
f SSymbol = {- SSymbol s in scope -}

Since: base-4.18.0.0

pattern SChar :: forall c. () => KnownChar c => SChar c Source #

A explicitly bidirectional pattern synonym relating an SChar to a KnownChar constraint.

As an expression: Constructs an explicit SChar c value from an implicit KnownChar c constraint:

SChar @c :: KnownChar c => SChar c

As a pattern: Matches on an explicit SChar c value bringing an implicit KnownChar c constraint into scope:

f :: SChar c -> ..
f SChar = {- SChar c in scope -}

Since: base-4.18.0.0

fromSNat :: SNat n -> Integer Source #

Return the Integer corresponding to n in an SNat n value. The returned Integer is always non-negative.

For a version of this function that returns a Natural instead of an Integer, see fromSNat in GHC.TypeNats.

Since: base-4.18.0.0

fromSSymbol :: SSymbol s -> String Source #

Return the String corresponding to s in an SSymbol s value.

Since: base-4.18.0.0

fromSChar :: SChar c -> Char Source #

Return the Char corresponding to c in an SChar c value.

Since: base-4.18.0.0

withSomeSNat :: forall rep (r :: TYPE rep). Integer -> (forall n. Maybe (SNat n) -> r) -> r Source #

Attempt to convert an Integer into an SNat n value, where n is a fresh type-level natural number. If the Integer argument is non-negative, invoke the continuation with Just sn, where sn is the SNat n value. If the Integer argument is negative, invoke the continuation with Nothing.

For a version of this function where the continuation uses 'SNat n instead of Maybe (SNat n)@, see withSomeSNat in GHC.TypeNats.

Since: base-4.18.0.0

withSomeSSymbol :: forall rep (r :: TYPE rep). String -> (forall s. SSymbol s -> r) -> r Source #

Convert a String into an SSymbol s value, where s is a fresh type-level symbol.

Since: base-4.18.0.0

withSomeSChar :: forall rep (r :: TYPE rep). Char -> (forall c. SChar c -> r) -> r Source #

Convert a Char into an SChar c value, where c is a fresh type-level character.

Since: base-4.18.0.0

withKnownNat :: forall n rep (r :: TYPE rep). SNat n -> (KnownNat n => r) -> r Source #

Convert an explicit SNat n value into an implicit KnownNat n constraint.

Since: base-4.18.0.0

withKnownSymbol :: forall s rep (r :: TYPE rep). SSymbol s -> (KnownSymbol s => r) -> r Source #

Convert an explicit SSymbol s value into an implicit KnownSymbol s constraint.

Since: base-4.18.0.0

withKnownChar :: forall c rep (r :: TYPE rep). SChar c -> (KnownChar c => r) -> r Source #

Convert an explicit SChar c value into an implicit KnownChar c constraint.

Since: base-4.18.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 UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) Source #

This type family yields type-level Just storing the first character of a symbol and its tail if it is defined and Nothing otherwise.

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