[Haskell-cafe] Is Harper right that Haskell cannot model the natural numbers?
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