jawarren:
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?
It shouldn't actually require new data structures, just new types (with no inhabiting values). such as, data Zero data Succ a So there are no values of this type (other than bottom). That is, you can just see 'data' here as a way of producing new types to play with in the type checker. -- Don