[Haskell-cafe] Re: [Haskell] Type-Level Naturals Like Prolog?

[Greg Buchholz]

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. "