On 13 Jul 2006, at 06:25, Jared Warren 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)

I don't think this can be what you mean: it implies that any y is the successor of zero, and that any y with a successor is a successor of x.

Why can't Haskell (with extensions) do type-level Peano naturals in the same fashion?

It can! (Well, depending on what you mean by "the same".)

{-# OPTIONS -fglasgow-exts #-}

data Zero data Succ n

class Natural n where toInt :: n -> Int

instance Natural Zero where toInt _ = 0

instance Natural n => Natural (Succ n) where toInt _ = succ (toInt (undefined :: n))

Incidentally, I think the thing you were trying to write was more like the following:

class IsZero x instance IsZero Zero

class IsSucc x y instance IsSucc Zero (Succ Zero) instance IsSucc m n => IsSucc (Succ m) (Succ n)

instance IsZero n => Natural n where toInt _ = 0

instance (Natural m, IsSucc m n) => Natural n where toInt _ = succ (toInt (undefined :: m))

This fails, because the two declarations of instances of Natural are illegal ("There must be at least one non-type-variable in the instance head", whereas in both cases there is just the type variable n in the instance head). The typechecker suggests -fallow-undecidable-instances, but this provokes a different error message: duplicate instances for Natural n. Jeremy

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 Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell

Jeremy.Gibbons@comlab.ox.ac.uk Oxford University Computing Laboratory, TEL: +44 1865 283508 Wolfson Building, Parks Road, FAX: +44 1865 273839 Oxford OX1 3QD, UK. URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html