Changes between Version 4 and Version 5 of TypeNats/Operations


Ignore:
Timestamp:
Jan 27, 2011 5:22:20 AM (4 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Operations

    v4 v5  
    1919== Inverse Operations == 
    2020 
    21 Using the basic operations and GHC's equality constraints it is also possible to express 
    22 some additional constraints, corresponding to the inverses (when defined) of the above functions: 
    23 {{{ 
    24 Constraint     | 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 Note that we need some form of relational notation to capture the partiality of the 
    33 inverses.  In GHC, using (~) seems like a natural choice.  If we'd introduced (-) 
    34 as another type function, we have a few choices, none of which seem particularly attractive: 
    35   * accept some ill defined "types" like (1 - 2), 
    36   * come up with a "completion" for the type function (e.g., by defining (1 - 2) ~ 0), 
    37   * automatically generate additional constraints which would ensure that types are well-defined, somehow. 
    38  
    39 While the relational notation may look a bit verbose, in practice we can often completely avoid it. 
    40 For example, consider that we are writing which needs to split an array of bytes into an array of 
    41 words.  We might give the function the following type: 
     21Our system does not have explicit functions for subtraction, division, logs, or roots.  However, we can get essentially the same functionality by combining the existing type functions with (implicit or explicit) equality constraints.  Consider, for example, the following type: 
    4222{{{ 
    4323bytesToWords :: Array (8 * w) Word8 -> Array w Word64 
    4424}}} 
    45 So, in effect, we perform a "division" by multiplying the argument. 
     25In this type we are basically dividing the size of the input array by 8.  Note, however, that we have expressed this by specifying that the array has to be a multiple of 8, which avoids the need for partiality. 
    4626 
    4727