I wrote:
Nice, lots of fun! Wouldn't it be more convenient to allow them to be signed?
John Meacham wrote:
Well, a couple reasons. One is that Natural numbers are a pretty useful type in and of themselves, often times when used with lazy evaluation. The other is that it is unclear what semantics lazy signed numbers would have...
True. I was thinking of the sign at the beginning - which means, essentially, the same as what you already have. The real only differences are: - Zero really means 0, not "0 or negative". - In certain special cases where you happen to know that the result should be a certain negative number, you get that In particular, the scrictness properties - which you have already so carefully worked out for the case of the naturals - do not change. Of course, you can then easily restrict to the naturals when you want that. -Yitz