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

Donald Bruce Stewart dons at cse.unsw.edu.au
Tue Jul 18 01:21:20 EDT 2006


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


More information about the Haskell-Cafe mailing list