basement-0.0.12: Foundation scrap box of array & string
Safe HaskellNone
LanguageHaskell2010

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 :: forall (n :: Nat) proxy. 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 #

Addition of type-level naturals.

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

Instances details
type NatNumMaxBound Char # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Char = 1114111
type NatNumMaxBound Int # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int8 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int8 = 127
type NatNumMaxBound Int16 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int16 = 32767
type NatNumMaxBound Int32 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int32 = 2147483647
type NatNumMaxBound Int64 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Int64 = 9223372036854775807
type NatNumMaxBound Word # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word8 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word16 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word16 = 65535
type NatNumMaxBound Word32 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word32 = 4294967295
type NatNumMaxBound Word64 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word64 = 18446744073709551615
type NatNumMaxBound Char7 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word128 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word128 = 340282366920938463463374607431768211455
type NatNumMaxBound Word256 # 
Instance details

Defined in Basement.Nat

type NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935
type NatNumMaxBound (Zn n) # 
Instance details

Defined in Basement.Bounded

type NatNumMaxBound (Zn n) = n
type NatNumMaxBound (Zn64 n) # 
Instance details

Defined in Basement.Bounded

type NatNumMaxBound (Zn64 n) = n
type NatNumMaxBound (CountOf x) # 
Instance details

Defined in Basement.Types.OffsetSize

type NatNumMaxBound (Offset x) # 
Instance details

Defined in Basement.Types.OffsetSize

Constraint

type family NatInBoundOf ty n where ... #

Check if a Nat is in bounds of another integral / natural types

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