Changes between Version 2 and Version 3 of TypeNats/Operations


Ignore:
Timestamp:
Jan 17, 2011 11:44:26 PM (5 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