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

[Jared Warren]

Thank you to everyone for the responses. I guess what I should have
clarified is that I know how Peano numbers are *normally* encoded in
the type language (I am very familiar with the HList library), but I
would like to know why the type language appears to require data
structures to do so while [Idealised] Prolog has none.

Niklas Broberg helpfully corrected my Prolog:

> That is not a valid encoding of peano numbers in prolog, so I think
> that's where your problems stem from. :-)
>
> % defining natural numbers
> natural(zero).
> natural(s(X)) :- natural(X).
>
> % translate to integers
> toInt(zero, 0).
> toInt(s(X), N) :- toInt(X, Y), N is Y + 1.

Thank you. I can now more precisely state that what I'm trying to
figure out is: what is 's', a predicate or a data structure? If it's a
predicate, where are its instances? If not, what is the difference
between the type language and Prolog such that the type language
requires data structures?