[Haskell-cafe] positive Int

[Neil Mitchell]

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 <clawsie at fastmail.fm> 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>