Jared Warren wrote:

Haskell's type checking language is a logical programming language. The canonical logical language is Prolog. Why can't Haskell (with extensions) do type-level Peano naturals in the same fashion? The code would be something like:

Also of possible interest, _Fun with Functional Dependencies_... http://www.cs.chalmers.se/~hallgren/Papers/wm01.html "This paper illustrates how Haskell's type class system can be used to express computations. Since computations on the type level are performed by the type checker, these computations are static (i.e., performed at compile-time), and, since the type system is decidable, they always terminate. Haskell thus provides a means to express static computations, and has a clear distinction between static and dynamic computations. "