haskus-utils-types-1.5: Haskus types utility modules

Safe HaskellSafe
LanguageHaskell2010

Haskus.Utils.Types.Nat

Contents

Description

Type-level Nat

Synopsis

Documentation

data Nat #

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

natValue :: forall (n :: Nat) a. (KnownNat n, Num a) => a Source #

Get a Nat value

natValue' :: forall (n :: Nat). KnownNat n => Word Source #

Get a Nat value as a Word

class KnownNat (n :: Nat) #

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

data SomeNat where #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

SomeNat :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat 
Instances
Eq SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool #

(/=) :: SomeNat -> SomeNat -> Bool #

Ord SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering #

(<) :: SomeNat -> SomeNat -> Bool #

(<=) :: SomeNat -> SomeNat -> Bool #

(>) :: SomeNat -> SomeNat -> Bool #

(>=) :: SomeNat -> SomeNat -> Bool #

max :: SomeNat -> SomeNat -> SomeNat #

min :: SomeNat -> SomeNat -> SomeNat #

Read SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat #

readList :: ReadS [SomeNat] #

readPrec :: ReadPrec SomeNat #

readListPrec :: ReadPrec [SomeNat] #

Show SomeNat

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS #

show :: SomeNat -> String #

showList :: [SomeNat] -> ShowS #

someNatVal :: Natural -> SomeNat #

Convert an integer into an unknown type-level natural.

Since: base-4.10.0.0

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

We either get evidence that this function was instantiated with the same type-level numbers, or Nothing.

Since: base-4.7.0.0

Comparisons

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

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

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 (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ True infix 4 #

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

type family NatEq a b :: Nat where ... Source #

Type equality to Nat

Equations

NatEq a a = 1 
NatEq a b = 0 

type family NatNotEq a b :: Nat where ... Source #

Type inequality to Nat

Equations

NatNotEq a a = 0 
NatNotEq a b = 1 

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

Max of two naturals

Equations

Max a b = If (a <=? b) b a 

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

Min of two naturals

Equations

Min a b = If (a <=? b) a b 

type family IsZero (n :: Nat) :: Nat where ... Source #

Return 1 if 0, and 0 otherwise

Equations

IsZero 0 = 1 
IsZero _ = 0 

type family IsNotZero (n :: Nat) :: Nat where ... Source #

Return 0 if 0, and 1 otherwise

Equations

IsNotZero 0 = 0 
IsNotZero _ = 1 

Operations

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

Addition of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

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

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Log2 (a :: Nat) :: Nat where ... #

Log base 2 (round down) of natural numbers. Log 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

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

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

Helpers

type family NatBitCount (n :: Nat) :: Nat where ... Source #

Number of bits (>= 1) required to store a Nat value

>>> natValue' @(NatBitCount 0)
1

>>> natValue' @(NatBitCount 1)
1

>>> natValue' @(NatBitCount 2)
2

>>> natValue' @(NatBitCount 5)
3

>>> natValue' @(NatBitCount 15)
4

>>> natValue' @(NatBitCount 16)
5

Equations

NatBitCount 0 = 1 
NatBitCount n = NatBitCount' (n + 1) (Log2 (n + 1))