basement-0.0.10: Foundation scrap box of array & string

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

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

class KnownNat (n :: Nat) 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.

Since: base-4.7.0.0

Minimal complete definition

natSing

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

Since: base-4.7.0.0

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

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 Source #

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

Addition of type-level naturals.

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

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