Safe Haskell	None
Language	Haskell2010

Basement.Nat

Contents

Nat convertion
Maximum bounds
Constraint

Synopsis

data Nat
class KnownNat (n :: Nat)
natVal :: KnownNat n => proxy n -> Integer
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True
type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
type family (a :: Nat) + (b :: Nat) :: Nat where ...
type family (a :: Nat) * (b :: Nat) :: Nat where ...
type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
type family (a :: Nat) - (b :: Nat) :: Nat where ...
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
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
type family NatNumMaxBound ty :: Nat
type family NatInBoundOf ty n where ...
type family NatWithinBound ty (n :: Nat) where ...

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 #

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

natValInt :: forall n proxy. (KnownNat n, NatWithinBound Int n) => proxy n -> Int Source #

natValInt8 :: forall n proxy. (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8 Source #

natValInt16 :: forall n proxy. (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16 Source #

natValInt32 :: forall n proxy. (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32 Source #

natValInt64 :: forall n proxy. (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64 Source #

natValWord :: forall n proxy. (KnownNat n, NatWithinBound Word n) => proxy n -> Word Source #

natValWord8 :: forall n proxy. (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8 Source #

natValWord16 :: forall n proxy. (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16 Source #

natValWord32 :: forall n proxy. (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32 Source #

natValWord64 :: forall n proxy. (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64 Source #

Maximum bounds

type family NatNumMaxBound ty :: Nat Source #

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

Instances

type NatNumMaxBound Char Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Char = 1114111
type NatNumMaxBound Int Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Int = NatNumMaxBound Int64
type NatNumMaxBound Int8 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Int8 = 127
type NatNumMaxBound Int16 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Int16 = 32767
type NatNumMaxBound Int32 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Int32 = 2147483647
type NatNumMaxBound Int64 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Int64 = 9223372036854775807
type NatNumMaxBound Word Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word = NatNumMaxBound Word64
type NatNumMaxBound Word8 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word8 = 255
type NatNumMaxBound Word16 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word16 = 65535
type NatNumMaxBound Word32 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word32 = 4294967295
type NatNumMaxBound Word64 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word64 = 18446744073709551615
type NatNumMaxBound Char7 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Char7 = 127
type NatNumMaxBound Word128 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word128 = 340282366920938463463374607431768211455
type NatNumMaxBound Word256 Source #
Instance details Defined in Basement.Nat type NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935
type NatNumMaxBound (Zn n) Source #
Instance details Defined in Basement.Bounded type NatNumMaxBound (Zn n) = n
type NatNumMaxBound (Zn64 n) Source #
Instance details Defined in Basement.Bounded type NatNumMaxBound (Zn64 n) = n
type NatNumMaxBound (CountOf x) Source #
Instance details Defined in Basement.Types.OffsetSize type NatNumMaxBound (CountOf x) = NatNumMaxBound Int
type NatNumMaxBound (Offset x) Source #
Instance details Defined in Basement.Types.OffsetSize type NatNumMaxBound (Offset x) = NatNumMaxBound Int

Constraint

type family NatInBoundOf ty n where ... Source #

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 ... Source #

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