[Haskell-cafe] Re: [Haskell] Type-Level Naturals Like Prolog?

[Donald Bruce Stewart]

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 at haskell.org, more appropriate)