Type arithmetic
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
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.