Basement.Nat

Documentation

data Nat :: *

(Kind) This is the kind of type-level natural numbers.

Instances

type (==) Nat a b

type (==) Nat a b = EqNat a b

class KnownNat (n :: Nat)

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

natVal :: KnownNat n => proxy n -> Integer

Since: 4.7.0.0

type (<=) (x :: Nat) (y :: Nat) = (~) Bool ((<=?) x y) True infix 4

Comparison of type-level naturals, as a constraint.

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... 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.

type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6

Addition of type-level naturals.

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7

Multiplication of type-level naturals.

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8

Exponentiation of type-level naturals.

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6

Subtraction of type-level naturals.

Since: 4.7.0.0

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

Nat convertion

natValNatural :: forall n proxy. KnownNat n => proxy n -> Natural

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 :: Nat

Get Maximum bounds of different Integral / Natural types related to Nat

Instances

type NatNumMaxBound Char

type NatNumMaxBound Char = 1114111

type NatNumMaxBound Int

type NatNumMaxBound Int = NatNumMaxBound Int64

type NatNumMaxBound Int8

type NatNumMaxBound Int8 = 127

type NatNumMaxBound Int16

type NatNumMaxBound Int16 = 32767

type NatNumMaxBound Int32

type NatNumMaxBound Int32 = 2147483647

type NatNumMaxBound Int64

type NatNumMaxBound Int64 = 9223372036854775807

type NatNumMaxBound Word

type NatNumMaxBound Word = NatNumMaxBound Word64

type NatNumMaxBound Word8

type NatNumMaxBound Word8 = 255

type NatNumMaxBound Word16

type NatNumMaxBound Word16 = 65535

type NatNumMaxBound Word32

type NatNumMaxBound Word32 = 4294967295

type NatNumMaxBound Word64

type NatNumMaxBound Word64 = 18446744073709551615

type NatNumMaxBound Char7

type NatNumMaxBound Char7 = 127

type NatNumMaxBound Word128

type NatNumMaxBound Word128 = 340282366920938463463374607431768211455

type NatNumMaxBound Word256

type NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935

type NatNumMaxBound (CountOf x)

type NatNumMaxBound (CountOf x) = NatNumMaxBound Int

type NatNumMaxBound (Offset x)

type NatNumMaxBound (Offset x) = NatNumMaxBound Int

Constraint

type family NatInBoundOf ty n where ...

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 family NatWithinBound ty (n :: Nat) where ...

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

Equations

NatWithinBound ty n = If (NatInBoundOf ty n) (() ~ ()) (TypeError (((Text "Natural " :<>: ShowType n) :<>: Text " is out of bounds for ") :<>: ShowType ty))