

## TypeLevel Operations









Currently, we provide the following typelevel operations on natural numbers:






```wiki



(<=) :: Nat > Nat > Prop  Comparison



(+) :: Nat > Nat > Nat  Addition



(*) :: Nat > Nat > Nat  Multiplication



(^) :: Nat > Nat > Nat  Exponentiation



```









Notes:






 `(<=)` is a 2parameter class (that's what we mean by the "kind" Prop),



 `(+)`, `(*)`, and `(^)` are type functions.



 Programmers may not provide custom instances of these classes/typefamilies.









The operations correspond to the usual operations on natural numbers.






## Inverse Operations









Using the basic operations and GHC's equality constraints it is also possible to express



some additional constraints, corresponding to the inverses (when defined) of the above functions:






```wiki



type family m ^ n :: Nat



type family m * n :: Nat



type family m + n :: Nat



class m <= n



``` 


\ No newline at end of file 


Constraint  Alternative Interpretation  Example (x "input", y "output")



++



(a + b) ~ c  Subtraction: (c  b) ~ a  Decrement by 8: x ~ (y + 8)



(a * b) ~ c  Division: (c / b) ~ a  Divide by 8: x ~ (y * 8)



(a ^ b) ~ c  Log at base: Log a c ~ b  Log base 2: x ~ (2 ^ y)



(a ^ b) ~ c  Nthroot: Root b c ~ a  Square root: x ~ (y ^ 2)



```









Note that we need some form of relational notation to capture the partiality of the



inverses. In GHC, using (\~) seems like a natural choice. If we'd introduced ()



as another type function, we have a few choices, none of which seem particularly attractive:






 accept some ill defined "types" like (1  2),



 come up with a "completion" for the type function (e.g., by defining (1  2) \~ 0),



 automatically generate additional constraints which would ensure that types are welldefined, somehow.









While the relational notation may look a bit verbose, in practice we can often completely avoid it.



For example, consider that we are writing which needs to split an array of bytes into an array of



words. We might give the function the following type:






```wiki



bytesToWords :: Array (8 * w) Word8 > Array w Word64



```









So, in effect, we perform a "division" by multiplying the argument.






## Solving Constraints 


\ No newline at end of file 