[Haskell-cafe] positive Int

Michael Vanier mvanier at cs.caltech.edu
Thu Aug 2 17:13:00 EDT 2007


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.


More information about the Haskell-Cafe mailing list