basement-0.0.10: Foundation scrap box of array & string

Basement.Nat

Synopsis

# Documentation

data Nat #

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

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: base-4.7.0.0

Minimal complete definition

natSing

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

Since: base-4.7.0.0

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

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

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 #

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Comparison of type-level naturals, as a function.

Since: base-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
 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Char = 1114111 # Instance detailsDefined in Basement.Nat # Instance detailsDefined in Basement.Nat type NatNumMaxBound Int8 = 127 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Int16 = 32767 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Int32 = 2147483647 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Int64 = 9223372036854775807 # Instance detailsDefined in Basement.Nat # Instance detailsDefined in Basement.Nat type NatNumMaxBound Word8 = 255 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Word16 = 65535 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Word32 = 4294967295 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Word64 = 18446744073709551615 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Char7 = 127 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Word128 = 340282366920938463463374607431768211455 # Instance detailsDefined in Basement.Nat type NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935 type NatNumMaxBound (Zn n) # Instance detailsDefined in Basement.Bounded type NatNumMaxBound (Zn n) = n type NatNumMaxBound (Zn64 n) # Instance detailsDefined in Basement.Bounded type NatNumMaxBound (Zn64 n) = n type NatNumMaxBound (CountOf x) # Instance detailsDefined in Basement.Types.OffsetSize type NatNumMaxBound (Offset x) # Instance detailsDefined in Basement.Types.OffsetSize

# 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))