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 Natural
- type Nat = Natural
- 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 (<=?) m n = OrdCond (Compare m n) 'True 'True 'False
- 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 :: Natural) (n :: Natural) :: Ordering
- cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b
- type family Div (m :: Nat) (n :: Nat) :: Nat
- type family Mod (m :: Nat) (n :: Nat) :: Nat
- type family Log2 (m :: Nat) :: Nat
Nat Kind
Natural number
Invariant: numbers <= 0xffffffffffffffff use the NS
constructor
Instances
Data Natural # | Since: base-4.8.0.0 |
Defined in Data.Data Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Natural -> c Natural # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Natural # toConstr :: Natural -> Constr # dataTypeOf :: Natural -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Natural) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Natural) # gmapT :: (forall b. Data b => b -> b) -> Natural -> Natural # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r # gmapQ :: (forall d. Data d => d -> u) -> Natural -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Natural -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Natural -> m Natural # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural # | |
Bits Natural # | Since: base-4.8.0 |
Defined in GHC.Bits Methods (.&.) :: Natural -> Natural -> Natural # (.|.) :: Natural -> Natural -> Natural # xor :: Natural -> Natural -> Natural # complement :: Natural -> Natural # shift :: Natural -> Int -> Natural # rotate :: Natural -> Int -> Natural # setBit :: Natural -> Int -> Natural # clearBit :: Natural -> Int -> Natural # complementBit :: Natural -> Int -> Natural # testBit :: Natural -> Int -> Bool # bitSizeMaybe :: Natural -> Maybe Int # shiftL :: Natural -> Int -> Natural # unsafeShiftL :: Natural -> Int -> Natural # shiftR :: Natural -> Int -> Natural # unsafeShiftR :: Natural -> Int -> Natural # rotateL :: Natural -> Int -> Natural # | |
Enum Natural # | Since: base-4.8.0.0 |
Ix Natural # | Since: base-4.8.0.0 |
Defined in GHC.Ix | |
Num Natural # | Note that Since: base-4.8.0.0 |
Read Natural # | Since: base-4.8.0.0 |
Integral Natural # | Since: base-4.8.0.0 |
Defined in GHC.Real | |
Real Natural # | Since: base-4.8.0.0 |
Defined in GHC.Real Methods toRational :: Natural -> Rational # | |
Show Natural # | Since: base-4.8.0.0 |
PrintfArg Natural # | Since: base-4.8.0.0 |
Defined in Text.Printf | |
Eq Natural | |
Ord Natural | |
KnownNat n => HasResolution (n :: Nat) # | For example, |
Defined in Data.Fixed Methods resolution :: p n -> Integer # | |
type Compare (a :: Natural) (b :: Natural) # | |
Defined in Data.Type.Ord |
A type synonym for Natural
.
Prevously, 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
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 #
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) #
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 comparable types, as a constraint.
Since: base-4.16.0.0
type (<=?) m n = OrdCond (Compare m n) 'True 'True 'False infix 4 #
Comparison (<=) of comparable types, as a function.
Since: base-4.16.0.0
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 :: Natural) (n :: Natural) :: Ordering #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b #
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 (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