| Maintainer | gatlin@niltag.net |
|---|---|
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Peano
Description
Definition of type-level Peano numerals along with type operators to inspect and manipulate them.
Synopsis
- data Natural (n :: Type)
- data Z
- data S (n :: k)
- class ReifyNatural (n :: Type) where
- reifyNatural :: Natural n
- type (<) a b = LessThan a b ~ 'True
- class LT (a :: k1) (b :: k2) where
- type (<=) a b = (LessThanOrEqual a b ~ 'True, Minus b a)
- class LTE (a :: k1) (b :: k2) where
- type LessThanOrEqual a b :: Bool
- class Plus (x :: Type) (y :: Type) where
- class Minus (x :: Type) (y :: Type) where
Natural numbers
data Natural (n :: Type) Source #
Natural numbers paired with type-level natural numbers. These terms each act as a witness for a particular natural.
Instances
| ReifyNatural Z Source # | |
| Minus x Z Source # | |
| Plus x Z Source # | |
| Replicable Z (x :: k) Source # | |
| LT Z Z Source # | |
| LTE Z Z Source # | |
| LT Z (S m :: Type) Source # | |
| LTE Z (S m :: Type) Source # | |
| LT (S n :: Type) Z Source # | |
| LTE (S n :: Type) Z Source # | |
| Functor t => Cross (S Z) t Source # | |
| type x + Z Source # | |
| type x - Z Source # | |
| type Replicate Z (x :: k) Source # | |
| type LessThan Z Z Source # | |
| type LessThanOrEqual Z Z Source # | |
Defined in Peano | |
| type LessThan Z (S m :: Type) Source # | |
| type LessThanOrEqual Z (S m :: Type) Source # | |
| type LessThan (S n :: Type) Z Source # | |
| type LessThanOrEqual (S n :: Type) Z Source # | |
Instances
| LT Z (S m :: Type) Source # | |
| LTE Z (S m :: Type) Source # | |
| LT (S n :: Type) Z Source # | |
| LTE (S n :: Type) Z Source # | |
| LT n m => LT (S n :: Type) (S m :: Type) Source # | |
| LTE (S n :: Type) (S m :: Type) Source # | |
| Plus x y => Plus x (S y) Source # | |
| Replicable n x => Replicable (S n) (x :: k) Source # | |
| ReifyNatural n => ReifyNatural (S n) Source # | |
| (Cross (S n) t, Functor t, Functor (Nested (NestedNTimes (S n) t))) => Cross (S (S n)) t Source # | |
| Functor t => Cross (S Z) t Source # | |
| Minus x y => Minus (S x) (S y) Source # | |
| type LessThan Z (S m :: Type) Source # | |
| type LessThanOrEqual Z (S m :: Type) Source # | |
| type LessThan (S n :: Type) Z Source # | |
| type LessThanOrEqual (S n :: Type) Z Source # | |
| type LessThan (S n :: Type) (S m :: Type) Source # | |
| type LessThanOrEqual (S n :: Type) (S m :: Type) Source # | |
Defined in Peano | |
| type x + (S y) Source # | |
| type Replicate (S n) (x :: k) Source # | |
| type (S x) - (S y) Source # | |
class ReifyNatural (n :: Type) where Source #
Given a context expecting a particular natural, we can manufacture it from the ether.
Methods
reifyNatural :: Natural n Source #
Instances
| ReifyNatural Z Source # | |
| ReifyNatural n => ReifyNatural (S n) Source # | |
Partial ordering
Less-than
class LT (a :: k1) (b :: k2) Source #
Type-level < test.
Less-than-or-equal
type (<=) a b = (LessThanOrEqual a b ~ 'True, Minus b a) Source #
This constraint is a more succinct way of requiring that
a be less than or equal to b.
class LTE (a :: k1) (b :: k2) Source #
Type-level <= test.
Associated Types
type LessThanOrEqual a b :: Bool Source #