Changes between Version 1 and Version 2 of TypeNats/Operations


Ignore:
Timestamp:
Jan 17, 2011 11:20:48 PM (3 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