Safe Haskell | None |
---|---|
Language | Haskell2010 |
Foundation.Primitive.Nat
- data Nat :: *
- class KnownNat n
- natVal :: KnownNat n => proxy n -> Integer
- type (<=) x y = (~) Bool ((<=?) x y) True
- type family a <=? b :: Bool
- type family a + b :: Nat
- type family a * b :: Nat
- type family a ^ b :: Nat
- type family a - b :: Nat
- type family CmpNat a b :: Ordering
- natValInt :: forall n proxy. (KnownNat n, NatWithinBound Int n) => proxy n -> Int
- natValInt8 :: forall n proxy. (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8
- natValInt16 :: forall n proxy. (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16
- natValInt32 :: forall n proxy. (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32
- natValInt64 :: forall n proxy. (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64
- natValWord :: forall n proxy. (KnownNat n, NatWithinBound Word n) => proxy n -> Word
- natValWord8 :: forall n proxy. (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8
- natValWord16 :: forall n proxy. (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16
- natValWord32 :: forall n proxy. (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32
- natValWord64 :: forall n proxy. (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64
- type family NatNumMaxBound ty
- type family NatInBoundOf ty n
- type NatWithinBound ty n = NatInBoundOf ty n ~ True
Documentation
data Nat :: *
(Kind) This is the kind of type-level natural numbers.
class KnownNat n
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: 4.7.0.0
Minimal complete definition
natSing
type (<=) x y = (~) Bool ((<=?) x y) True infix 4
Comparison of type-level naturals, as a constraint.
type family a <=? b :: 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.
Nat convertion
natValInt :: forall n proxy. (KnownNat n, NatWithinBound Int n) => proxy n -> Int
natValInt8 :: forall n proxy. (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8
natValInt16 :: forall n proxy. (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16
natValInt32 :: forall n proxy. (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32
natValInt64 :: forall n proxy. (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64
natValWord :: forall n proxy. (KnownNat n, NatWithinBound Word n) => proxy n -> Word
natValWord8 :: forall n proxy. (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8
natValWord16 :: forall n proxy. (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16
natValWord32 :: forall n proxy. (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32
natValWord64 :: forall n proxy. (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64
Maximum bounds
type family NatNumMaxBound ty
Get Maximum bounds of different Integral / Natural types related to Nat
Equations
NatNumMaxBound Int64 = 9223372036854775807 | |
NatNumMaxBound Int32 = 2147483647 | |
NatNumMaxBound Int16 = 32767 | |
NatNumMaxBound Int8 = 127 | |
NatNumMaxBound Word64 = 18446744073709551615 | |
NatNumMaxBound Word32 = 4294967295 | |
NatNumMaxBound Word16 = 65535 | |
NatNumMaxBound Word8 = 255 | |
NatNumMaxBound Int = NatNumMaxBound Int64 | |
NatNumMaxBound Word = NatNumMaxBound Word64 |
Constraint
type family NatInBoundOf ty n
Check if a Nat is in bounds of another integral / natural types
Equations
NatInBoundOf Integer n = True | |
NatInBoundOf Natural n = True | |
NatInBoundOf ty n = n <=? NatNumMaxBound ty |
type NatWithinBound ty n = NatInBoundOf ty n ~ True
Constraint to check if a natural is within a specific bounds of a type.
i.e. given a Nat n
, is it possible to convert it to ty
without losing information