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

Richard O'Keefe ok at cs.otago.ac.nz
Tue May 3 05:25:29 CEST 2011

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.

Fair enough, but what about

	data Nat = Zero | Succ !Nat

where the constructors *are* strict?  It's perfectly good Haskell 98
as far as I can see.  Now "Nat" itself isn't _quite_ a model of the
naturals because it includes bottom, but then an SML function
returning nat can also fail, so arguably SML's nat could or should be
thought of as including bottom too.

What am I missing?

More information about the Haskell-Cafe mailing list