"Richard O'Keefe" <o...@cs.otago.ac.nz> writes:

> In one of his blog posts, Robert Harper claims that the natural numbers
> are not definable in Haskell.
>
> SML   datatype nat = ZERO | SUCC of nat
> Haskell       data Nat = Zero | Succ Nat
>
> differ in that the SML version has strict constructors, and so only
> finite instances of nat can be constructed, whereas Haskell has
> lazy constructors, so
>       inf = Succ inf
> is constructible, but that's not a natural number, and it isn't
> bottom either, so this is not a model of the natural numbers.

I think Prof. Harper criticism is weak. Defining the set of natural
numbers is not easy. What does he understand as natural number? Peano
axioms fail in similar fashion given that PA has non standard models
which include elements similar to your inf.

You may used other approaches like second order logic or von Neumann
ordinals, but they have their own set of drawbacks.

Regards,
Emilio


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to