Copyright | (c) Kyle McKean, 2016 |
---|---|
License | MIT |
Maintainer | mckean.kylej@gmail.com |
Stability | experimental |
Portability | Portable |
Safe Haskell | None |
Language | Haskell2010 |
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.
Singleton natural numbers, unlike inductive natural numbers this data type has O(1) toInt.
type family ToKnownNat (a :: Nat) :: Nat where ... #
ToKnownNat Z = 0 | |
ToKnownNat (S n) = 1 + ToKnownNat n |
type family FromKnownNat (a :: Nat) :: Nat where ... #
FromKnownNat 0 = Z | |
FromKnownNat n = S (FromKnownNat (n - 1)) |
fromKnownNat :: forall proxy n. IsNat (FromKnownNat n) => proxy n -> SNat (FromKnownNat n) #
type family (a :: Nat) - (b :: Nat) :: Nat where ... #
Type level monus. This is not subtraction as natural numbers do not form a group.
monus :: SNat a -> SNat b -> SNat (a - b) #
This function returns zero if the result would normally be negative.
type family Cmp (a :: Nat) (b :: Nat) :: Ordering where ... #
lte :: SNat n -> SNat m -> Maybe (LTE n m) #
This function should be used at runtime to prove n <= m.