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
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
