[Haskell-cafe] Is Harper right that Haskell cannot model the natural numbers?

[Emilio Jesús Gallego Arias]

"Richard O'Keefe" <ok at 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