foundation-0.0.13: Alternative prelude with batteries and no dependencies

Safe HaskellNone
LanguageHaskell2010

Foundation.Primitive.Nat

Contents

Synopsis

Documentation

data Nat :: *

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

Instances

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 <=? b :: Bool 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 + b :: Nat infixl 6

Addition of type-level naturals.

type family a * b :: Nat infixl 7

Multiplication of type-level naturals.

type family a ^ b :: Nat infixr 8

Exponentiation of type-level naturals.

type family a - b :: Nat infixl 6

Subtraction of type-level naturals.

Since: 4.7.0.0

type family CmpNat a b :: Ordering

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

Nat convertion

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

Maximum bounds

type family NatNumMaxBound ty

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

Equations

NatNumMaxBound Int64 = 9223372036854775807 
NatNumMaxBound Int32 = 2147483647 
NatNumMaxBound Int16 = 32767 
NatNumMaxBound Int8 = 127 
NatNumMaxBound Word64 = 18446744073709551615 
NatNumMaxBound Word32 = 4294967295 
NatNumMaxBound Word16 = 65535 
NatNumMaxBound Word8 = 255 
NatNumMaxBound Int = NatNumMaxBound Int64 
NatNumMaxBound Word = NatNumMaxBound Word64 

Constraint

type family NatInBoundOf ty n

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 NatWithinBound ty n = NatInBoundOf ty n ~ True

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