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

[Jared Warren]

> >> % 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. :-/)