jawarren:

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

Perhaps these will be useful? http://www.haskell.org/haskellwiki/Peano_numbers http://www.haskell.org/haskellwiki/Type_arithmetic and a bit of stuff here http://www.haskell.org/haskellwiki/Smart_constructors Cheers, Don (P.S. moved to haskell-cafe@haskell.org, more appropriate)