[Haskell-cafe] Re: [Haskell] Type-Level Naturals Like Prolog?
Niklas Broberg
niklas.broberg at gmail.com
Thu Jul 13 04:20:24 EDT 2006
On 7/13/06, Jared Warren <jawarren at gmail.com> 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)
That is not a valid encoding of peano numbers in prolog, so I think
that's where your problems stem from. :-)
% defining natural numbers
natural(zero).
natural(s(X)) :- natural(X).
% translate to integers
toInt(zero, 0).
toInt(s(X), N) :- toInt(X, Y), N is Y + 1.
In the same style of reasoning for Haskell, we would define
> data Zero
> data Succ x
>
> class Natural x
> instance Natural Zero
> instance (Natural x) => Natural (Succ x)
>
> class Natural x => ToInt x where
> toInt :: x -> Int
>
> instance ToInt Zero where
> toInt _ = 0
>
> instance (ToInt x) => ToInt (Succ x) where
> toInt _ = toInt (undefined :: x) + 1
Or we could add the toInt method directly to the Natural class like
you did above. So yes, we can mimic (some of) prolog in Haskell's type
language. :-)
/Niklas
More information about the Haskell-Cafe
mailing list