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