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?