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

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 type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Convert an integer into an unknown type-level natural.

Since: base-4.7.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

(Kind) An integer that may be negative.

This class gives the (value-level) integer associated with a type-level integer. There are instances of this class for every concrete natural: 0, 1, 2, etc. There are also instances of this class for every negated natural, such as Neg 1.

Get the value associated with a type-level integer

Get the value associated with a type-level integer. The difference between this function and intVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

This type represents unknown type-level integers.

Since: 0.1.1

Convert an integer into an unknown type-level integer.

Since: 0.1.1

Type constructor for a rational

This class gives the (value-level) rational associated with a type-level rational. There are instances of this class for every combination of a concrete integer and concrete natural.

Get the value associated with a type-level rational

Get the value associated with a type-level rational. The difference between this function and ratVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

This type represents unknown type-level integers.

Since: 0.1.1

Convert a rational into an unknown type-level rational.

Since: 0.1.1

Reduce a type-level rational into its canonical form

Since: 0.1.4

Boolean type-level equals. Useful for e.g. If (x ==? 0)

Boolean type-level not-equals.

Boolean comparison of two type-level numbers

Equality constraint, used as e.g. (x == 3) => _

Not-equal constraint

The absolute value of a type-level number

Since: 0.1.4

The result of negating a TInt

Since: 0.1.4

The reciprocal of a type-level number

Since: 0.1.4

Round a type-level number towards negative infinity

Since: 0.1.4

Round a type-level number towards positive infinity

Since: 0.1.4

Round a type-level number towards zero

Since: 0.1.4

The sum of two type-level numbers

The difference of two type-level numbers

For the difference of two naturals a and b, a-b is also a natural, so only exists for a >= b.

The product of two type-level numbers.

Due to changes in GHC 8.6, using this operator infix and unqualified requires the NoStarIsType language extension to be active. See the GHC 8.6.x migration guide for details: https://ghc.haskell.org/trac/ghc/wiki/Migration/8.6

The ratio of two type-level numbers

A type-level number raised to an integer power. For Nat powers, the result kind is the same as the base. For TInt powers, the result kind is Rat.

Since: 0.1.4

The quotient and remainder of a type-level integer and a natural number. For a negative dividend, the remainder part is positive such that x = q*y + r @since 0.1.4

The quotient and remainder of a type-level integer and a natural number. For a negative dividend, the remainder part is negative such that x = q*y + r @since 0.1.4

The quotient of a type-level integer and a natural number.

Since: 0.1.4

The remainder of a type-level integer and a natural number For a negative number, behaves similarly to mod. @since 0.1.4

The integer part of the result of dividing an integer by a natural number

Since: 0.1.4

The remainder of the result of dividing an integer by a natural number

Since: 0.1.4

The greatest common divisor of two type-level integers

Since: 0.1.4

The floor of the logarithm of a type-level number NB. unlike Log2, Log n 0 here is a type error.

Since: 0.1.4

The floor of the logarithm base 2 of a type-level number. Note that unlike Log2, this errors on Log2 0.

Since: 0.1.4

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

Concatenation of type-level symbols.

Since: base-4.10.0.0

Comparison of type-level symbols, as a function.

Since: base-4.7.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

This type represents unknown type-level symbols.

Convert a string into an unknown type-level symbol.

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

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.