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
Richard O'Keefe o...@cs.otago.ac.nz writes:
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
On 11-05-02 11:25 PM, Richard O'Keefe wrote:
Fair enough, but what about
data Nat = Zero | Succ !Nat
It works. I say, Harper forgot it.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
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,