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