wiki:TypeNats/Operations

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)