Type arithmetic (or type-level computations) are calculations over types.

Haskell lacks type-level lambdas and thus, one could say it also lacks native support for type arithmetic. However, it is possible to use multiparameter type classes (originally devised to support multiparameter function overloading) to implement type-level computations.

Some inmediate applications of type-level programming in Haskell are:

• Heterogeneous lists and extensible records.
• Emulation of dependent types, e.g. statically-safe vectors, in which the vector bounds can be checked at compile-time.

During the talk we will go through a simplified implementation of type-level Booleans and Naturals.