Of course, you can always do this: data Nat = Zero | Succ Nat but it's not very much fun to work with, and not very efficient. Mike David Roundy wrote:
On Thu, Aug 02, 2007 at 12:29:46PM -0700, brad clawsie wrote:
On Thu, Aug 02, 2007 at 12:17:06PM -0700, brad clawsie wrote:
as far as i know, the haskell standard does not define a basic Int type that is limited to positive numbers.
would a type of this kind not potentially allow us to make stronger verification statements about certain functions?
for example, 'length' returns an Int, but in reality it must always return a value 0 or greater. a potential counter-argument would be the need to possibly redefine Ord etc for this more narrow type... i suppose one could also say that the range [0..] of return values is *implicit* in the function definition, so there is little value in explicitly typing it given all of the hassle of specifying a new typeclass etc
This would be a very nice type to have (natural numbers), but is a tricky type to work with. Subtraction, for instance, wouldn't be possible as a complete function... or one might say that if you included subtraction you're even less safe: negative results either must throw an exception or be impossible to catch. You might point out that overflow in an Int is similar (uncatchable), but overflow is much harder to accidentally run into than negative values.
A nicer option would be some sort of "extra" proof rather than a new type. But that sort of work is rather tricky, as I understand it.