Modulebasement-0.0.16Haskell2010

Basement.Nat

3 types
1 class
12 values

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

typetype Nat = Natural

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.20.2.0 · Data.Fixed
For example, Fixed 1000 will give you a Fixed with a resolution of 1000.

classclass KnownNat (n :: Nat) where

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

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

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

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

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

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

Addition of type-level naturals.

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

Multiplication of type-level naturals.

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

Exponentiation of type-level naturals.

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

Subtraction of type-level naturals.

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

Comparison of type-level naturals, as a function.

Nat convertion

11 declarations

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

1 declaration

familytype family NatNumMaxBound ty :: Nat

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

2 declarations

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

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