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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
