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

[Peter Gammie]

On 03/05/2011, at 1:25 PM, Richard O'Keefe wrote:

> 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?

Do read the comments attached to the blog post (and also maybe at reddit).

I believe the traditional model for ML-like languages  in denotational semantics is to lift the type returned by a function. So ML's "Nat" type is taken to be an inductively-defined set (with the discrete order) and your divergent ML function really has type a -> Nat_{lift} for whatever type a you had in mind. I think Moggi's encoding into monads makes this clear - you use the Maybe/Evaluation/Strict monad to handle divergent arguments.

cheers
peter

-- 
http://peteg.org/