Hi John, I wrote:
- Zero really means 0, not "0 or negative"
You wrote:
Actually, zero does mean zero. There is no such thing as negative numbers in the naturals so it doesn't make sense to say '0 or negative'.
Well, then, "0 or error", or "0 or nothing". It clearly does not mean zero.
Subtraction is necessarily defined differently of course.
As described in the referenced paper, (yes, an enjoyable read, thanks) this is for convenience only. No one is claiming that 1 - 2 == 0 in the naturals. It is just undefined. But we find that returning Zero rather than raising an exception happens to do the right thing for certain common usages of the naturals. Anyway, my point is that you have done two good things here that are orthogonal to each other: a good lazy integral type, and a good naturals type. So why not make the laziness available also for cases where "1 - 2 == 0" does _not_ do the right thing? data LazyInteger = IntZero | IntSum Bool Integer LazyInteger or data LazyInteger = LazyInteger Bool Nat or whatever. Thanks, Yitz