fast-nats-0.1.0.1: Natural Numbers with no overhead

Data.Nat

Description

Synopsis

# Documentation

data Nat #

Inductive natural numbers used only for type level operations.

Constructors

 Z S Nat

Instances

 # MethodstestCoercion :: f a -> f b -> Maybe (Coercion SNat a b) # # MethodstestEquality :: f a -> f b -> Maybe ((SNat :~: a) b) #

data SNat n #

Singleton natural numbers, unlike inductive natural numbers this data type has O(1) toInt.

Instances

 # MethodstestCoercion :: f a -> f b -> Maybe (Coercion SNat a b) # # MethodstestEquality :: f a -> f b -> Maybe ((SNat :~: a) b) # Show (SNat n) # MethodsshowsPrec :: Int -> SNat n -> ShowS #show :: SNat n -> String #showList :: [SNat n] -> ShowS #

class IsNat n where #

This class is used to emulate agda and idris' implicit parameters. It also can be used to turn a Nat into an SNat.

Minimal complete definition

witness

Methods

witness :: SNat n #

Instances

 # Methods KnownNat (ToKnownNat (S n)) => IsNat (S n) # Methodswitness :: SNat (S n) #

natToInt :: SNat n -> Int #

Transform a SNat into an Int. This has a post condition that the Int is not negative.

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

Transform a GHC.Typelit Nat into an inductive Nat.

Equations

 ToKnownNat Z = 0 ToKnownNat (S n) = 1 + ToKnownNat n

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

Transform a GHC.Typelit Nat into an inductive Nat.

Equations

 FromKnownNat 0 = Z FromKnownNat n = S (FromKnownNat (n - 1))

fromKnownNat :: forall proxy n. IsNat (FromKnownNat n) => proxy n -> SNat (FromKnownNat n) #

Generate a SNat from a GHC.Typelit Nat.

The smallest SNat.

succ :: SNat n -> SNat (S n) #

Add one to an SNat.

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

Equations

 Z + n = n (S n) + m = S (n + m)

plus :: SNat a -> SNat b -> SNat (a + b) #

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

Type level predecessor function.

Equations

 Pred Z = Z Pred (S n) = n

pred :: SNat n -> SNat (Pred n) #

Predecessor function, it does nothing with the natural is zero.

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

Type level monus. This is not subtraction as natural numbers do not form a group.

Equations

 n - Z = n Z - m = m (S n) - (S m) = n - m

monus :: SNat a -> SNat b -> SNat (a - b) #

This function returns zero if the result would normally be negative.

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

Type level multiplication.

Equations

 Z * n = Z (S n) * m = m + (n * m)

times :: SNat a -> SNat b -> SNat (a * b) #

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

Type level exponentiation.

Equations

 base ^ Z = S Z base ^ (S n) = base * (base ^ n)

power :: SNat a -> SNat b -> SNat (a ^ b) #

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

Type level minimum.

Equations

 Min Z m = Z Min (S Z) Z = Z Min (S n) (S m) = S (Min n m)

minimum :: SNat a -> SNat b -> SNat (Min a b) #

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

Type level maximum.

Equations

 Max Z m = m Max (S Z) Z = S Z Max (S n) (S m) = S (Max n m)

maximum :: SNat a -> SNat b -> SNat (Max a b) #

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

Type level comparsion. This function returns a promoted Ordering.

This function is only useful when you know the natural numbers at compile time. If you need to compare naturals at runtime use Compare.

Equations

 Cmp Z Z = EQ Cmp (S n) Z = GT Cmp Z (S m) = LT Cmp (S n) (S m) = Cmp n m

data IsZero :: Nat -> Type where #

Proof that a natural number is zero.

Constructors

 SIsZ :: IsZero Z

isZero :: SNat n -> Maybe (IsZero n) #

This is a runtime function used to check if a Nat is zero.

data LTE :: Nat -> Nat -> Type where #

Constructive <= if n <= m then exists (k : Nat). n + k = m

Constructors

 SLTE :: SNat y -> LTE (y + x) x

Instances

 Show (LTE n m) # MethodsshowsPrec :: Int -> LTE n m -> ShowS #show :: LTE n m -> String #showList :: [LTE n m] -> ShowS #

lte :: SNat n -> SNat m -> Maybe (LTE n m) #

This function should be used at runtime to prove n <= m.

data Compare :: Nat -> Nat -> Type where #

Constructive compare if n < m then exists (k : Nat). n + k + 1 = m if n == m then n = m if n > m then exists (k : Nat). n = m + k + 1

Constructors

 SLT :: SNat y -> Compare x (S y + x) SEQ :: Compare x x SGT :: SNat y -> Compare (S y + x) x

Instances

 Show (Compare n m) # MethodsshowsPrec :: Int -> Compare n m -> ShowS #show :: Compare n m -> String #showList :: [Compare n m] -> ShowS #

cmp :: SNat a -> SNat b -> Compare a b #

This function should be used at runtime to compare two Nats