[Haskell-cafe] Re: [Haskell] Type-Level Naturals Like Prolog?
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(x), succ(x,y) :- natural(y)
> And I believe (but cannot confirm):
> 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(s(X)) :- natural(X).
% translate to integers
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
More information about the Haskell-Cafe