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.

@since base-4.16.0.0

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

@since base-4.7.0.0

@since base-4.7.0.0

@since base-4.8.0.0

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

@since base-4.7.0.0

@since base-4.8.0.0

@since base-4.16.0.0

This type represents unknown type-level natural numbers.

@since base-4.10.0.0

This type represents unknown type-level symbols.

Convert an integer into an unknown type-level natural.

@since base-4.7.0.0

Convert a string into an unknown type-level symbol.

@since base-4.7.0.0

Convert a character into an unknown type-level char.

@since base-4.16.0.0

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

@since base-4.7.0.0

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

@since base-4.7.0.0

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

@since base-4.16.0.0

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

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

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

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

@since base-4.16.0.0

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

@since base-4.16.0.0

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

@since base-4.16.0.0

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

@since base-4.16.0.0

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

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

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

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

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

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

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

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

@since base-4.18.0.0

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

@since base-4.18.0.0

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

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

@since base-4.18.0.0

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

@since base-4.18.0.0

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

@since base-4.18.0.0

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

@since base-4.18.0.0

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

@since base-4.18.0.0

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

@since base-4.16.0.0

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

@since base-4.16.0.0

Addition of type-level naturals.

@since base-4.7.0.0

Multiplication of type-level naturals.

@since base-4.7.0.0

Exponentiation of type-level naturals.

@since base-4.7.0.0

Subtraction of type-level naturals.

@since base-4.7.0.0

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

@since base-4.11.0.0

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

@since base-4.11.0.0

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

@since base-4.11.0.0

Concatenation of type-level symbols.

@since base-4.10.0.0

Comparison of type-level naturals, as a function.

@since base-4.7.0.0

Comparison of type-level symbols, as a function.

@since base-4.7.0.0

Comparison of type-level characters.

@since base-4.16.0.0

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

@since base-4.16.0.0

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

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

@since base-4.16.0.0

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

@since base-4.16.0.0

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

A description of a custom type error.