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.
- data Nat
- data SNat n
- class IsNat n where
- natToInt :: SNat n -> Int
- type family ToKnownNat (a :: Nat) :: Nat where ...
- type family FromKnownNat (a :: Nat) :: Nat where ...
- fromKnownNat :: forall proxy n. IsNat (FromKnownNat n) => proxy n -> SNat (FromKnownNat n)
- zero :: SNat Z
- succ :: SNat n -> SNat (S n)
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- plus :: SNat a -> SNat b -> SNat (a + b)
- type family Pred (a :: Nat) :: Nat where ...
- pred :: SNat n -> SNat (Pred n)
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- monus :: SNat a -> SNat b -> SNat (a - b)
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- times :: SNat a -> SNat b -> SNat (a * b)
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- power :: SNat a -> SNat b -> SNat (a ^ b)
- type family Min (a :: Nat) (b :: Nat) :: Nat where ...
- minimum :: SNat a -> SNat b -> SNat (Min a b)
- type family Max (a :: Nat) (b :: Nat) :: Nat where ...
- maximum :: SNat a -> SNat b -> SNat (Max a b)
- type family Cmp (a :: Nat) (b :: Nat) :: Ordering where ...
- data IsZero :: Nat -> Type where
- isZero :: SNat n -> Maybe (IsZero n)
- data LTE :: Nat -> Nat -> Type where
- lte :: SNat n -> SNat m -> Maybe (LTE n m)
- data Compare :: Nat -> Nat -> Type where
- cmp :: SNat a -> SNat b -> Compare a b
Documentation
Inductive natural numbers used only for type level operations.
Instances
Singleton natural numbers, unlike inductive natural numbers this data type has O(1) toInt.
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
type family ToKnownNat (a :: Nat) :: Nat where ... Source #
Equations
ToKnownNat Z = 0 | |
ToKnownNat (S n) = 1 + ToKnownNat n |
type family FromKnownNat (a :: Nat) :: Nat where ... Source #
Equations
FromKnownNat 0 = Z | |
FromKnownNat n = S (FromKnownNat (n - 1)) |
fromKnownNat :: forall proxy n. IsNat (FromKnownNat n) => proxy n -> SNat (FromKnownNat n) Source #
pred :: SNat n -> SNat (Pred n) Source #
Predecessor function, it does nothing with the natural is zero.
type family (a :: Nat) - (b :: Nat) :: Nat where ... Source #
Type level monus. This is not subtraction as natural numbers do not form a group.
monus :: SNat a -> SNat b -> SNat (a - b) Source #
This function returns zero if the result would normally be negative.
type family Cmp (a :: Nat) (b :: Nat) :: Ordering where ... Source #
isZero :: SNat n -> Maybe (IsZero n) Source #
This is a runtime function used to check if a Nat
is zero.
data LTE :: Nat -> Nat -> Type where Source #
Constructive <= if n <= m then exists (k : Nat). n + k = m
lte :: SNat n -> SNat m -> Maybe (LTE n m) Source #
This function should be used at runtime to prove n <= m.