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

[Niklas Broberg]

On 7/13/06, Jared Warren <jawarren at gmail.com> wrote:
> Haskell's type checking language is a logical programming language.
> The canonical logical language is Prolog. However, Idealised Prolog
> does not have data structures, and does Peano numbers like:
>
>   natural(zero).
>   natural(x), succ(x,y) :- natural(y)
>
> And I believe (but cannot confirm):
>
>   succ(zero,y).
>   succ(x,y) :- succ(y,z)

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.

In the same style of reasoning for Haskell, we would define

> data Zero
> data Succ x
>
> class Natural x
> instance Natural Zero
> instance (Natural x) => Natural (Succ x)
>
> class Natural x => ToInt x where
>  toInt :: x -> Int
>
> instance ToInt Zero where
>  toInt _ = 0
>
> instance (ToInt x) => ToInt (Succ x) where
>  toInt _ = toInt (undefined :: x) + 1

Or we could add the toInt method directly to the Natural class like
you did above. So yes, we can mimic (some of) prolog in Haskell's type
language. :-)

/Niklas