Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
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 module.
Since: base-4.10.0.0
Synopsis
- data Natural
- type Nat = Natural
- class KnownNat (n :: Nat) where
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- someNatVal :: Natural -> SomeNat
- sameNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b)
- decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b)
- data SNat (n :: Nat)
- pattern SNat :: () => KnownNat n => SNat n
- fromSNat :: forall (n :: Nat). SNat n -> Natural
- withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r
- withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
- type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint)
- type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False
- type family (a :: Natural) + (b :: Natural) :: Natural where ...
- type family (a :: Natural) * (b :: Natural) :: Natural where ...
- type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
- type family (a :: Natural) - (b :: Natural) :: Natural where ...
- type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ...
- cmpNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b
- type family Div (a :: Natural) (b :: Natural) :: Natural where ...
- type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
- type family Log2 (a :: Natural) :: Natural where ...
Nat Kind
Instances
A type synonym for Natural
.
Previously, this was an opaque data type, but it was changed to a type synonym.
Since: base-4.16.0.0
Linking type and value level
class KnownNat (n :: Nat) where 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
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 :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (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
decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Source #
We either get evidence that this function was instantiated with the same type-level numbers, or that the type-level numbers are distinct.
Since: base-4.19.0.0
Singleton values
A value-level witness for a type-level natural number. This is commonly
referred to as a singleton type, as for each n
, there is a single value
that inhabits the type
(aside from bottom).SNat
n
The definition of SNat
is intentionally left abstract. To obtain an SNat
value, use one of the following:
- The
natSing
method ofKnownNat
. - The
SNat
pattern synonym. - The
withSomeSNat
function, which creates anSNat
from aNatural
number.
Since: base-4.18.0.0
Instances
TestCoercion SNat | Since: base-4.18.0.0 |
Defined in GHC.Internal.TypeNats | |
TestEquality SNat | Since: base-4.18.0.0 |
Defined in GHC.Internal.TypeNats | |
Show (SNat n) | Since: base-4.18.0.0 |
Eq (SNat n) | Since: base-4.19.0.0 |
Ord (SNat n) | Since: base-4.19.0.0 |
Defined in GHC.Internal.TypeNats |
pattern SNat :: () => KnownNat n => SNat n Source #
A explicitly bidirectional pattern synonym relating an SNat
to a
KnownNat
constraint.
As an expression: Constructs an explicit
value from an
implicit SNat
n
constraint:KnownNat
n
SNat @n ::KnownNat
n =>SNat
n
As a pattern: Matches on an explicit
value bringing
an implicit SNat
n
constraint into scope:KnownNat
n
f :: SNat
n -> ..
f SNat = {- KnownNat n in scope -}
Since: base-4.18.0.0
Functions on type literals
type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 Source #
Comparison (<=) of comparable types, as a constraint.
Since: base-4.16.0.0
type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 Source #
Comparison (<=) of comparable types, as a function.
Since: base-4.16.0.0
type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 Source #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 Source #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 Source #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 Source #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Source #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
cmpNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b Source #
Like sameNat
, but if the numbers aren't equal, this additionally
provides proof of LT or GT.
Since: base-4.16.0.0
type family Div (a :: Natural) (b :: Natural) :: Natural where ... 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