Changes between Version 2 and Version 3 of TypeNats/Operations


Ignore:
Timestamp:
Jan 17, 2011 11:44:26 PM (3 years ago)
Author:
diatchki
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeNats/Operations

    v2 v3  
    3030}}} 
    3131 
     32Note that we need some form of relational notation to capture the partiality of the 
     33inverses.  In GHC, using (~) seems like a natural choice.  If we'd introduced (-) 
     34as 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 
     39While the relational notation may look a bit verbose, in practice we can often completely avoid it. 
     40For example, consider that we are writing which needs to split an array of bytes into an array of 
     41words.  We might give the function the following type: 
     42{{{ 
     43bytesToWords :: Array (8 * w) Word8 -> Array w Word64 
     44}}} 
     45So, in effect, we perform a "division" by multiplying the argument. 
    3246 
    3347 
    34