Type arithmetic - HaskellWiki

Type arithmetic (or type-level computation) are calculations on the type-level, often implemented in Haskell using functional dependencies to represent functions. A simple example of type-level computation are operations on 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) Many other representations

[ruicc]

type-level computation

[hengsu]

Type理論による計算の実現