[Haskell] Type-Level Naturals Like Prolog?

[Jeremy Gibbons]

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

Jeremy.Gibbons at 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