[Haskell-cafe] Re: Type-Level Naturals Like Prolog?
jawarren at gmail.com
Tue Jul 18 15:12:09 EDT 2006
> >> % 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
> 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
"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
I would love to read your article! (I can give you a [forthcoming?]
citation if I ever get through this part of my thesis. :-/)
More information about the Haskell-Cafe