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

[Bulat Ziganshin]

Hello Jared,

Tuesday, July 18, 2006, 9:05:09 AM, you wrote:

>> % 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


The more important difference is what Prolog is _logic_ programming
language and there you can use unification and backtracking in
functions' definitions. Haskell is _not_ logic programming language so
you can't define functions what use these techniques. The humor,
though, is that Haskell's multi-parameter type classes defines logic
programming language, but at the _type_ level. Values of this
language is _types_ instead of ordinary values. And naturally,
instead of data constructors - _type_ constructors are used to construct
new type values and in the unification operations. So, you can't use
"Just" in this language, but "Maybe" can be used. GHC also supports
nullary data definitions which defines just type constructor without
data constructors:

data Zero
data Succ a

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

-- 
Best regards,
 Bulat                            mailto:Bulat.Ziganshin at gmail.com