basement-0.0.1: Foundation scrap box of array & string

Safe HaskellNone
LanguageHaskell2010

Basement.Nat

Contents

Synopsis

Documentation

data Nat :: * #

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

Instances

type (==) Nat a b 
type (==) Nat a b = EqNat a b

class KnownNat n #

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: 4.7.0.0

Minimal complete definition

natSing

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

Since: 4.7.0.0

type (<=) x y = (~) Bool ((<=?) x y) True infix 4 #

Comparison of type-level naturals, as a constraint.

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.

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

Multiplication of type-level naturals.

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

Exponentiation of type-level naturals.

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

Subtraction of type-level naturals.

Since: 4.7.0.0

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

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

Nat convertion

natValNatural :: forall n proxy. KnownNat n => proxy n -> Natural Source #

natValCountOf :: forall n ty proxy. (KnownNat n, NatWithinBound (CountOf ty) n) => proxy n -> CountOf ty Source #

natValOffset :: forall n ty proxy. (KnownNat n, NatWithinBound (Offset ty) n) => proxy n -> Offset ty 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 where ... Source #

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

Equations

NatNumMaxBound Char = 1114111 
NatNumMaxBound Char7 = 127 
NatNumMaxBound Int64 = 9223372036854775807 
NatNumMaxBound Int32 = 2147483647 
NatNumMaxBound Int16 = 32767 
NatNumMaxBound Int8 = 127 
NatNumMaxBound Word256 = 115792089237316195423570985008687907853269984665640564039457584007913129639935 
NatNumMaxBound Word128 = 340282366920938463463374607431768211455 
NatNumMaxBound Word64 = 18446744073709551615 
NatNumMaxBound Word32 = 4294967295 
NatNumMaxBound Word16 = 65535 
NatNumMaxBound Word8 = 255 
NatNumMaxBound Int = NatNumMaxBound Int64 
NatNumMaxBound Word = NatNumMaxBound Word64 
NatNumMaxBound (CountOf x) = NatNumMaxBound Int 
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

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