GHC.TypeNats

base-4.11.1.0: Basic libraries

Safe Haskell | Trustworthy
Language | Haskell2010

GHC.TypeNats

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

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

Minimal complete definition

natSing

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

Since: base-4.10.0.0

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

Since: base-4.10.0.0

data SomeNat #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n) |

Instances

Eq SomeNat # | Since: base-4.7.0.0
Instance details Defined in GHC.TypeNats Methods (==) :: SomeNat -> SomeNat -> Bool Source # (/=) :: SomeNat -> SomeNat -> Bool Source #
Ord SomeNat # | Since: base-4.7.0.0
Instance details Defined in GHC.TypeNats Methods compare :: SomeNat -> SomeNat -> Ordering Source # (<) :: SomeNat -> SomeNat -> Bool Source # (<=) :: SomeNat -> SomeNat -> Bool Source # (>) :: SomeNat -> SomeNat -> Bool Source # (>=) :: SomeNat -> SomeNat -> Bool Source # max :: SomeNat -> SomeNat -> SomeNat Source # min :: SomeNat -> SomeNat -> SomeNat Source #
Read SomeNat # | Since: base-4.7.0.0
Instance details Defined in GHC.TypeNats Methods readsPrec :: Int -> ReadS SomeNat # readList :: ReadS [SomeNat] # readPrec :: ReadPrec SomeNat # readListPrec :: ReadPrec [SomeNat] #
Show SomeNat # | Since: base-4.7.0.0
Instance details Defined in GHC.TypeNats Methods showsPrec :: Int -> SomeNat -> ShowS # show :: SomeNat -> String # showList :: [SomeNat] -> ShowS #

someNatVal :: Natural -> SomeNat #

Convert an integer into an unknown type-level natural.

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

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Comparison of type-level naturals, as a function.

Since: base-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: base-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: base-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: base-4.11.0.0