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/