[Haskell-cafe] Clarification on proof section of HS: The Craft of
zednenem at psualum.com
Tue May 3 20:41:31 EDT 2005
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.
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 <zednenem at psualum.com> <http://www.eyrie.org/~zednenem/>
More information about the Haskell-Cafe