GHC.TypeLits

Safe Haskell	Safe
Language	Haskell2010

Kinds

data Natural

type Nat = Natural Source

A type synonym for Natural.

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

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

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer Source

Since: base-4.7.0.0

natVal' :: forall (n :: Nat). 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 :: Symbol) proxy. KnownSymbol n => proxy n -> String Source

Since: base-4.7.0.0

symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String Source

Since: base-4.8.0.0

class KnownChar (n :: Char) where Source

Since: base-4.16.0.0

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

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

data SomeNat Source

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

data SomeSymbol Source

This type represents unknown type-level symbols.

data SomeChar Source

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 :: Nat) (b :: Nat) 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 :: Symbol) (b :: Symbol) 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 :: Char) (b :: Char) 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

decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Source

We either get evidence that this function was instantiated with the same type-level numbers, or that the type-level numbers are distinct.

Since: base-4.19.0.0

decideSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Source

We either get evidence that this function was instantiated with the same type-level symbols, or that the type-level symbols are distinct.

Since: base-4.19.0.0

decideChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Source

We either get evidence that this function was instantiated with the same type-level characters, or that the type-level characters are distinct.

Since: base-4.19.0.0

data OrderingI (a :: k) (b :: k) where Source

Ordering data type for type literals that provides proof of their ordering.

Since: base-4.16.0.0

cmpNat :: forall (a :: Nat) (b :: Nat) 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 :: Symbol) (b :: Symbol) 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 :: Char) (b :: Char) 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

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

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

pattern SNat :: () => 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 = {- KnownNat n in scope -}

Since: base-4.18.0.0

pattern SSymbol :: () => 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 = {- KnownSymbol s in scope -}

Since: base-4.18.0.0

pattern SChar :: () => 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 = {- KnownChar c in scope -}

Since: base-4.18.0.0

fromSNat :: forall (n :: Nat). 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 :: forall (s :: Symbol). SSymbol s -> String Source

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

Since: base-4.18.0.0

fromSChar :: forall (c :: Char). SChar c -> Char Source

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

Since: base-4.18.0.0

withSomeSNat :: Integer -> (forall (n :: Nat). 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 :: String -> (forall (s :: Symbol). 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 :: Char -> (forall (c :: Char). 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 :: Nat) r. 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 :: Symbol) r. 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 :: Char) r. 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 :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 Source

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.0.0

type (<=?) (m :: k) (n :: k) = 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 (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 Source

Addition of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 Source

Multiplication of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 Source

Exponentiation of type-level naturals.

Since: base-4.7.0.0

type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 Source

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family Div (a :: Natural) (b :: Natural) :: Natural where ... 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 (a :: Natural) (b :: Natural) :: Natural where ... 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 (a :: Natural) :: Natural where ... 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 (a :: Symbol) (b :: Symbol) :: Symbol where ... Source

Concatenation of type-level symbols.

Since: base-4.10.0.0

type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Source

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... Source

Comparison of type-level symbols, as a function.

Since: base-4.7.0.0

type family CmpChar (a :: Char) (b :: Char) :: Ordering where ... Source

Comparison of type-level characters.

Since: base-4.16.0.0

type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ... 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) where ... 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 (a :: Char) :: Natural where ... Source

Convert a character to its Unicode code point (cf. ord)

Since: base-4.16.0.0

type family NatToChar (a :: Natural) :: Char where ... 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.