Data.Nat

Fast natural numbers, you can learn more about these types from agda and idris' standard libary.

Documentation

data Nat

Inductive natural numbers used only for type level operations.

Constructors

Z

S Nat

Instances

TestCoercion Nat SNat

Methods

testCoercion :: f a -> f b -> Maybe (Coercion SNat a b)

TestEquality Nat SNat

Methods

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

TestCoercion Nat SNat

Methods

testCoercion :: f a -> f b -> Maybe (Coercion SNat a b)

TestEquality Nat SNat

Methods

testEquality :: f a -> f b -> Maybe ((SNat :~: a) b)

Show (SNat n)

Methods

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

IsNat Z

Methods

witness :: SNat Z

KnownNat (ToKnownNat (S n)) => IsNat (S n)

Methods

witness :: 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.

zero :: SNat Z

The smallest SNat.

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

Add one to an SNat.

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

Type level addition of naturals.

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)

Methods

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

Methods

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