Changes between Version 1 and Version 2 of TypeNats/Operations


Ignore:
Timestamp:
Jan 17, 2011 11:20:48 PM (5 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Operations

    v1 v2  
    11== Type-Level Operations ==
    22
     3Currently, we provide the following type-level operations on natural numbers:
     4
    35{{{
    4 type family m ^ n :: Nat
    5 type family m * n :: Nat
    6 type family m + n :: Nat
    7 class m <= n
     6(<=) :: Nat -> Nat -> Prop    -- Comparison
     7(+)  :: Nat -> Nat -> Nat     -- Addition
     8(*)  :: Nat -> Nat -> Nat     -- Multiplication
     9(^)  :: Nat -> Nat -> Nat     -- Exponentiation
    810}}}
     11Notes:
     12  * {{{(<=)}}} is a 2-parameter class (that's what we mean by the "kind" Prop),
     13  * {{{(+)}}}, {{{(*)}}}, and {{{(^)}}} are type functions.
     14  * Programmers may not provide custom instances of these classes/type-families.
     15
     16The operations correspond to the usual operations on natural numbers.
     17
     18
     19== Inverse Operations ==
     20
     21Using the basic operations and GHC's equality constraints it is also possible to express
     22some additional constraints, corresponding to the inverses (when defined) of the above functions:
     23{{{
     24Constraint     | Alternative Interpretation    | Example (x "input", y "output")
     25---------------+-------------------------------+--------------------------------
     26(a + b) ~ c    | Subtraction: (c - b) ~ a      | Decrement by 8: x ~ (y + 8)
     27(a * b) ~ c    | Division:    (c / b) ~ a      | Divide by 8:    x ~ (y * 8)
     28(a ^ b) ~ c    | Log at base: Log  a c ~ b     | Log base 2:     x ~ (2 ^ y)
     29(a ^ b) ~ c    | Nth-root:    Root b c ~ a     | Square root:    x ~ (y ^ 2)
     30}}}
     31
     32
     33
     34