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

[Manuel M T Chakravarty]

In this context, I'd suggest to have a look at the POPL'06 paper "Fast and Loose Reasoning is Morally Correct"

 http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf

The paper is quite technical, so here the gist.  It says that if you formally proof that two Haskell expressions do the same thing by reasoning *as if* you were using a total language (one without non-termination), then the two expressions are also "morally the same" in Haskell.[1]  They formally define what "morally the same" means.  In particular, the Introduction says: "Our results justify the hand reasoning that functional programmers already perform, and can be applied in proof checkers and automated provers to justify ignoring ⊥-cases much of the time."

In other words, yes, 'Nat' in Haskell is not the same as the natural numbers as axiomised by Peano.  Does it matter?  Not really.

Manuel

PS: Given that ML is impure, a lot of equational reasoning in ML is also no more than morally correct.

[1] The paper doesn't show that statement for the entirety of Haskell, but for a core language with a comparable semantics using lifted types.

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.
> 
> 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?
> 
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe