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

unsafeWithSNatCo allows uses of coerce in its argument to see the real representation of SNat n, without undermining the type-safety of coerce elsewhere in the module.

See also the documentation for UnsafeSNat.

unsafeWithSSymbolCo allows uses of coerce in its argument to see the real representation of SSymbol s, without undermining the type-safety of coerce elsewhere in the module.

See also the documentation for UnsafeSSymbol.

unsafeWithSCharCo allows uses of coerce in its argument to see the real representation of SChar c, without undermining the type-safety of coerce elsewhere in the module.

See also the documentation for UnsafeSChar.

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.