GHC.TypeLits

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

A type synonym for Natural.

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

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

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.

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

This type represents unknown type-level natural numbers.

This type represents unknown type-level symbols.

Convert an integer into an unknown type-level natural.

Convert a string into an unknown type-level symbol.

Convert a character into an unknown type-level char.

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

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

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

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

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

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

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

Like sameNat, but if the numbers aren't equal, this additionally provides proof of LT or GT.

Like sameSymbol, but if the symbols aren't equal, this additionally provides proof of LT or GT.

Like sameChar, but if the Chars aren't equal, this additionally provides proof of LT or GT.

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

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

Addition of type-level naturals.

Multiplication of type-level naturals.

Exponentiation of type-level naturals.

Subtraction of type-level naturals.

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Concatenation of type-level symbols.

Comparison of type-level naturals, as a function.

Comparison of type-level symbols, as a function.

Comparison of type-level characters.

Extending a type-level symbol with a type-level character

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

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

Convert a Unicode code point to a character (cf. chr)

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

A description of a custom type error.