GHC.TypeNats (original) (raw)

Contents

• Nat Kind
• Linking type and value level
• Functions on type literals

Description

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

Synopsis

• data Nat
• class KnownNat (n :: Nat)
• natVal :: forall n proxy. KnownNat n => proxy n -> Natural
• natVal' :: forall n. KnownNat n => Proxy# n -> Natural
• data SomeNat = KnownNat n => SomeNat (Proxy n)
• someNatVal :: Natural -> SomeNat
• sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
• type (<=) x y = (x <=? y) ~ True
• type family (m :: Nat) <=? (n :: Nat) :: Bool
• type family (m :: Nat) + (n :: Nat) :: Nat
• type family (m :: Nat) * (n :: Nat) :: Nat
• type family (m :: Nat) ^ (n :: Nat) :: Nat
• type family (m :: Nat) - (n :: Nat) :: Nat
• type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
• type family Div (m :: Nat) (n :: Nat) :: Nat
• type family Mod (m :: Nat) (n :: Nat) :: Nat
• type family Log2 (m :: Nat) :: Nat

Nat Kind

data Nat #

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

Linking type and value level

class KnownNat (n :: Nat) 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: 4.7.0.0

Minimal complete definition

natSing

data SomeNat Source #

This type represents unknown type-level natural numbers.

Since: 4.10.0.0

Functions on type literals

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

Comparison of type-level naturals, as a constraint.

Since: 4.7.0.0

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

Comparison of type-level naturals, as a function. NOTE: The functionality for this function should be subsumed by [CmpNat](GHC-TypeNats.html#t:CmpNat "GHC.TypeNats"), 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 Source #

Addition of type-level naturals.

Since: 4.7.0.0

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

Multiplication of type-level naturals.

Since: 4.7.0.0

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

Exponentiation of type-level naturals.

Since: 4.7.0.0

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

Subtraction of type-level naturals.

Since: 4.7.0.0

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

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

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

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

Since: 4.11.0.0