W3cubDocs

/Haskell 8

GHC.TypeNats

Safe Haskell Trustworthy
Language Haskell2010

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

Nat Kind

data Nat Source

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

Minimal complete definition

natSing

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

Since: base-4.10.0.0

natVal' :: forall n. 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

Constructors

forall n.KnownNat n => SomeNat (Proxy n)
Instances
Instances details
Eq SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Ord SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Read SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Show SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

someNatVal :: Natural -> SomeNat Source

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

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 Source

Comparison of type-level naturals, as a constraint.

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

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Comparison of type-level naturals, as a function.

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

© The University of Glasgow and others
Licensed under a BSD-style license (see top of the page).
https://downloads.haskell.org/~ghc/8.8.3/docs/html/libraries/base-4.13.0.0/GHC-TypeNats.html