Hi Catch (www.cs.york.ac.uk/~ndm/catch) can infer that certain uses of numbers fit into the {Neg, Zero, One, Pos} abstraction - so for example it can infer that length returns {Zero, One, Pos}, but not Neg. If you then do:
xs !! length ys It will detect that length ys is natural, and will be safe. However, if you pass any arbitrary value as the index to !! it will warn of a possible pattern match error. You can of course use type Nat = Int, and write additional documentation, even if this documentation isn't a static guarantee. Thanks Neil On 8/2/07, brad clawsie <[EMAIL PROTECTED]> 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... > > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe