Benjamin Franksen writes:
On Wednesday 04 May 2005 01:32, Ben Rudiak-Gould wrote:
This doesn't work in Haskell because Haskell types aren't constructed in this way. It's harder to prove properties of types in Haskell (and fewer properties actually hold).
Could you explain why this is so? Or rather, what the appropriate technique is in Haskell? I assume it has to do with laziness but I have no idea how it enters the picture.
I suspect it's because Haskell types are non-strict by default.
Given
data Nat = Zero | Succ Nat
in a strict language, Succ _|_ == _|_. This is not the case in Haskell.
This isn't the case in Haskell, which is why we can do things like:
infinity = Succ infinity
Haskell lets you treat infinity mostly as though it were a normal value
of Nat. You can do arithmetic and compare it to finite values without
ever hitting bottom.
--
David Menendez