Is Harper right that Haskell cannot model the natural numbers?
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?
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/
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
"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.
I think Prof. Harper criticism is weak. Defining the set of natural numbers is not easy. What does he understand as natural number? Peano axioms fail in similar fashion given that PA has non standard models which include elements similar to your inf. You may used other approaches like second order logic or von Neumann ordinals, but they have their own set of drawbacks. Regards, Emilio
participants (5)
-
Albert Y. C. Lai -
egallego＠babel.ls.fi.upm.es -
Manuel M T Chakravarty -
Peter Gammie -
Richard O'Keefe