| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
GHC.TypeNats
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 = forall n.KnownNat n => SomeNat (Proxy n)
- someNatVal :: Natural -> SomeNat
- sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 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
(Kind) This is the kind of type-level natural numbers.
Instances
| KnownNat n => HasResolution (n :: Nat) # | For example, |
Defined in Data.Fixed Methods resolution :: p n -> Integer Source # | |
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
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
Instances
| Read SomeNat # | Since: base-4.7.0.0 |
| Show SomeNat # | Since: base-4.7.0.0 |
| Eq SomeNat # | Since: base-4.7.0.0 |
| Ord SomeNat # | Since: base-4.7.0.0 |
someNatVal :: Natural -> SomeNat Source #
Convert an integer into an unknown type-level natural.
Since: base-4.10.0.0
sameNat :: (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
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