[Haskell] Type-Level Naturals Like Prolog?

13 Jul 2006

      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)

Why can't Haskell (with extensions) do type-level Peano naturals in
the same fashion? The code would be something like:
...
data Zero
class Natural x where
  toInt :: x -> Integer
instance Natural Zero where
  toInt _ = 0
instance (Natural x, Succ x y) => Natural y where
  toInt y = undefined + 1
class Succ x y
instance Succ Zero y
instance Succ x y => Succ y z
zero = toInt (undefined :: Zero) -- THIS SUCCEEDS
one = toInt (undefined :: (Succ Zero x) => x) -- THIS FAILS
Thanks,
Jared Warren