Modulebasement-0.0.16Haskell2010

Basement.Nat

Contents

Nat convertion
Maximum bounds
Constraint

Synopsis

type Nat
class KnownNat
value natVal
type <=
type <=?
family +
family *
family ^
family -
family CmpNat
value natValNatural
value natValInt
value natValInt8
value natValInt16
value natValInt32
value natValInt64
value natValWord
value natValWord8
value natValWord16
value natValWord32
value natValWord64
family NatNumMaxBound
family NatInBoundOf
family NatWithinBound

Packagebasement-0.0.16
Exports24
LanguageHaskell2010
LicenceBSD-3-Clause
SourceTypeNats.hs

typetype Nat = Natural

Source#

A type synonym for Natural.

Previously, this was an opaque data type, but it was changed to a type synonym.

Instances1HasResolution

KnownNat n => HasResolution nDefined in base-4.23.0.0 · Data.Fixed
For example, Fixed 1000 will give you a Fixed with a resolution of 1000.

classclass KnownNat (n :: Nat) where

Source#

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.

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

Source#

typetype (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y)

Source#

Comparison (<=) of comparable types, as a constraint.

typetype (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False

Source#

Comparison (<=) of comparable types, as a function.

familytype family (+) (a :: Natural) (b :: Natural) :: Natural

Source#

Addition of type-level naturals.

familytype family (*) (a :: Natural) (b :: Natural) :: Natural

Source#

Multiplication of type-level naturals.

familytype family (^) (a :: Natural) (b :: Natural) :: Natural

Source#

Exponentiation of type-level naturals.

familytype family (-) (a :: Natural) (b :: Natural) :: Natural

Source#

Subtraction of type-level naturals.

familytype family CmpNat (a :: Natural) (b :: Natural) :: Ordering

Source#

Comparison of type-level naturals, as a function.

Nat convertion

valuenatValNatural :: KnownNat n => proxy n -> Natural

valuenatValInt :: (KnownNat n, NatWithinBound Int n) => proxy n -> Int

valuenatValInt8 :: (KnownNat n, NatWithinBound Int8 n) => proxy n -> Int8

valuenatValInt16 :: (KnownNat n, NatWithinBound Int16 n) => proxy n -> Int16

valuenatValInt32 :: (KnownNat n, NatWithinBound Int32 n) => proxy n -> Int32

valuenatValInt64 :: (KnownNat n, NatWithinBound Int64 n) => proxy n -> Int64

valuenatValWord :: (KnownNat n, NatWithinBound Word n) => proxy n -> Word

valuenatValWord8 :: (KnownNat n, NatWithinBound Word8 n) => proxy n -> Word8

valuenatValWord16 :: (KnownNat n, NatWithinBound Word16 n) => proxy n -> Word16

valuenatValWord32 :: (KnownNat n, NatWithinBound Word32 n) => proxy n -> Word32

valuenatValWord64 :: (KnownNat n, NatWithinBound Word64 n) => proxy n -> Word64

Maximum bounds

familytype family NatNumMaxBound ty :: Nat

Source#

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

Instances18NatNumMaxBound, …

type NatNumMaxBound Char7 = 127Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word128 = 340282366920938463463374607431768211455Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Int16 = 32767Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Int32 = 2147483647Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Int64 = 9223372036854775807Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Int8 = 127Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Char = 1114111Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Int = NatNumMaxBound Int64Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word = NatNumMaxBound Word64Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word16 = 65535Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word32 = 4294967295Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word64 = 18446744073709551615Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound Word8 = 255Defined in basement-0.0.16 · Basement.Nat
type NatNumMaxBound (Zn n) = nDefined in basement-0.0.16 · Basement.Bounded
type NatNumMaxBound (Zn64 n) = nDefined in basement-0.0.16 · Basement.Bounded
type NatNumMaxBound (CountOf x) = NatNumMaxBound IntDefined in basement-0.0.16 · Basement.Types.OffsetSize
type NatNumMaxBound (Offset x) = NatNumMaxBound IntDefined in basement-0.0.16 · Basement.Types.OffsetSize

Constraint

familytype family NatInBoundOf ty (n :: Nat) :: Bool 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

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