Copyright	(c) Kyle McKean, 2016
License	MIT
Maintainer	mckean.kylej@gmail.com
Stability	experimental
Portability	Portable
Safe Haskell	None
Language	Haskell2010

Data.Nat

Description

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

Synopsis

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