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...
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 sorry, yes i am talking to myself
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
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.
On Thu, Aug 02, 2007 at 02:08:33PM -0700, David Roundy wrote:
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...
Of course it would. It would just have the type Nat -> Nat -> Integer. This of course means that Nat wouldn't be an instance of Num. Tough luck, and one more reason for more fine-grained algebraic class hierarchy: Nat would be a semiring (as would booleans and finite sets and regular expressions and whatnot). Lauri
On 8/2/07, David Roundy
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...
There is a subtraction-like operation for naturals, where a - b = 0 if a <= b. This is analogous to the way that "drop n xs" returns [] if n
= length xs, but using it in a Num instance would probably violate too many assumptions.
The desire to support naturals was the motivation for including semirings in my Num refactoring thought-experiment. http://article.gmane.org/gmane.comp.lang.haskell.cafe/15141/
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.
Haskell 98 doesn't have such a type, no, but in today's libraries there is Data.Word.Word. Operations like subtraction will just wrap around when they would otherwise go negative, though ("All arithmetic is performed modulo 2^n").
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...
The main worry I can see with doing that is, would you need to keep explicitly converting between Int and Word? It might be possible to convert enough things to Word that it doesn't matter. You'd also break lots of programs, of course. Thanks Ian
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
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
On Fri, Aug 03, 2007 at 01:45:03AM +0100, Neil Mitchell wrote:
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.
I hope catch doesn't actually think that's safe, because it's not - set ys = xs = [1,2,3,4,5], you'll get an index out of range error. (Yes, I deliberately chose a list longer than 4 elements). Stefan
Hi
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.
I hope catch doesn't actually think that's safe, because it's not - set ys = xs = [1,2,3,4,5], you'll get an index out of range error. (Yes, I deliberately chose a list longer than 4 elements).
Of course, it doesn't, I abstracted for the sake of simplicity :-) The !! operator has two entirely separate pattern match errors, one is "negative index", one is "ran off the end of the list". The length xs will satisfy the first one by proving that length is always a natural, but the only proof of the other condition is that either the list is infinite, or that the index is Zero/One, and the list is bigger than this. Thanks Neil
participants (8)
-
brad clawsie -
David Menendez -
David Roundy -
Ian Lynagh -
Lauri Alanko -
Michael Vanier -
Neil Mitchell -
Stefan O'Rear