haskus-utils-types-1.6: Haskus types utility modules
Safe HaskellSafe-Inferred
LanguageHaskell2010

Haskus.Utils.Types.Nat

Description

Type-level Nat

Synopsis

Documentation

type Nat = Natural #

A type synonym for Natural.

Prevously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

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 #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n) 

Instances

Instances details
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 #

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 #

someNatVal :: Natural -> SomeNat #

Convert an integer into an unknown type-level natural.

Since: base-4.10.0.0

sameNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 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 :: Natural) (b :: Natural) :: Ordering where ... #

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 #

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

Since: base-4.16.0.0

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 #

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

Since: base-4.16.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 :: Natural) + (b :: Natural) :: Natural where ... infixl 6 #

Addition of type-level naturals.

Since: base-4.7.0.0

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

type family Mod (a :: Natural) (b :: Natural) :: Natural 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 :: Natural) :: Natural 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 :: Natural) (b :: Natural) :: Natural 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))