[Haskell-cafe] positive Int

[David Roundy]

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.
-- 
David Roundy
Department of Physics
Oregon State University