Type arithmetic
Jump to navigation
Jump to search
Type arithmetic is calculations on types using fundeps as functions.
A simple example is Peano numbers:
data Zero
data Succ a
class Add a b ab | a b -> ab, a ab -> b instance Add Zero b b instance (Add a b ab) => Add (Succ a) b (Succ ab)
However, many other representations of numbers are possible, including binary and balanced base three. Type arithmetic may also include type representations of boolean values and so on.