% 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's data structure, to be exact, it's data constructor - just like, for example, "Just" in Haskell. Haskell requires that all data constructors should be explicitly defined before they can be used. you can use "Just" to construct data values only if your program declares "Just" as data constructor with "data" definition like this:
data Maybe a = Just a | Nothing
Prolog is more liberate language and there you can use any data constructors without their explicit declarations, moreover, there is no such declarations anyway
[deletia]
i once said you about good paper on type-classes level programming. if you want, i can send you my unfinished article on this topic which shows correspondences between logic programming, type classes and GADTs
So predicates and data constructors have similar syntax but different semantics in Prolog? Say, for the sake of argument, if I wanted to do automatic translation, how would I tell which was which in a Prolog program? "Faking it: Simulating dependent types in Haskell" certainly explains *one* way to simulate dependent types, but I need to justify the existence of type constructors in an Idealised Haskell, so I must understand why the implementation in Prolog does not appear to be a literal translation. I would love to read your article! (I can give you a [forthcoming?] citation if I ever get through this part of my thesis. :-/)