GHC.TypeNats

Safe Haskell	Safe
Language	Haskell2010

Nat Kind

data Natural Source

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

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

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 -> Natural Source

Since: base-4.10.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural Source

Since: base-4.10.0.0

data SomeNat Source

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

someNatVal :: Natural -> SomeNat Source

Convert an integer into an unknown type-level natural.

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

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

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

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

fromSNat :: forall (n :: Nat). SNat n -> Natural Source

Return the Natural number corresponding to n in an SNat n value.

Since: base-4.18.0.0

withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r Source

Convert a Natural number into an SNat n value, where n is a fresh type-level natural number.

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

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 CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Source

Comparison of type-level naturals, as a function.

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

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