[Haskell-cafe] Clarification on proof section of HS: The Craft of FP

[David Menendez]

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 <zednenem at psualum.com> <http://www.eyrie.org/~zednenem/>