GHC.TypeNats

This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface for working with type-level naturals should be defined in a separate library.

Since: 4.10.0.0

Nat Kind

data Nat

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

Linking type and value level

class KnownNat (n :: Nat)

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: 4.7.0.0

Minimal complete definition

natSing

natVal :: forall n proxy. KnownNat n => proxy n -> Natural

Since: 4.10.0.0

natVal' :: forall n. KnownNat n => Proxy# n -> Natural

Since: 4.10.0.0

data SomeNat

This type represents unknown type-level natural numbers.

Since: 4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n)

Instances

Eq SomeNat

Since: 4.7.0.0

Methods

(==) :: SomeNat -> SomeNat -> Bool

(/=) :: SomeNat -> SomeNat -> Bool

Ord SomeNat

Since: 4.7.0.0

Methods

compare :: SomeNat -> SomeNat -> Ordering

(<) :: SomeNat -> SomeNat -> Bool

(<=) :: SomeNat -> SomeNat -> Bool

(>) :: SomeNat -> SomeNat -> Bool

(>=) :: SomeNat -> SomeNat -> Bool

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

Read SomeNat

Since: 4.7.0.0

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: 4.7.0.0

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

someNatVal :: Natural -> SomeNat

Convert an integer into an unknown type-level natural.

Since: 4.10.0.0

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)

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

Since: 4.7.0.0

Functions on type literals

type (<=) x y = (x <=? y) ~ True infix 4

Comparison of type-level naturals, as a constraint.

Since: 4.7.0.0

type family (m :: Nat) <=? (n :: Nat) :: Bool infix 4

Comparison of type-level naturals, as a function. NOTE: The functionality for this function should be subsumed by CmpNat, so this might go away in the future. Please let us know, if you encounter discrepancies between the two.

type family (m :: Nat) + (n :: Nat) :: Nat infixl 6

Addition of type-level naturals.

Since: 4.7.0.0

type family (m :: Nat) * (n :: Nat) :: Nat infixl 7

Multiplication of type-level naturals.

Since: 4.7.0.0

type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8

Exponentiation of type-level naturals.

Since: 4.7.0.0

type family (m :: Nat) - (n :: Nat) :: Nat infixl 6

Subtraction of type-level naturals.

Since: 4.7.0.0

type family CmpNat (m :: Nat) (n :: Nat) :: Ordering

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

type family Div (m :: Nat) (n :: Nat) :: Nat infixl 7

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

Since: 4.11.0.0

type family Mod (m :: Nat) (n :: Nat) :: Nat infixl 7

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

Since: 4.11.0.0

type family Log2 (m :: Nat) :: Nat

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

Since: 4.11.0.0