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