Version 2 (modified by diatchki, 3 years ago) (diff) |
---|

## Type-Level Operations

Currently, we provide the following type-level operations on natural numbers:

(<=) :: Nat -> Nat -> Prop -- Comparison (+) :: Nat -> Nat -> Nat -- Addition (*) :: Nat -> Nat -> Nat -- Multiplication (^) :: Nat -> Nat -> Nat -- Exponentiation

Notes:

`(<=)`is a 2-parameter class (that's what we mean by the "kind" Prop),`(+)`,`(*)`, and`(^)`are type functions.- Programmers may not provide custom instances of these classes/type-families.

The operations correspond to the usual operations on natural numbers.

## Inverse Operations

Using the basic operations and GHC's equality constraints it is also possible to express some additional constraints, corresponding to the inverses (when defined) of the above functions:

Constraint | Alternative Interpretation | Example (x "input", y "output") ---------------+-------------------------------+-------------------------------- (a + b) ~ c | Subtraction: (c - b) ~ a | Decrement by 8: x ~ (y + 8) (a * b) ~ c | Division: (c / b) ~ a | Divide by 8: x ~ (y * 8) (a ^ b) ~ c | Log at base: Log a c ~ b | Log base 2: x ~ (2 ^ y) (a ^ b) ~ c | Nth-root: Root b c ~ a | Square root: x ~ (y ^ 2)