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