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