A Quantity Type - Integer without the Negative #'s

Hi all, Is there a datatype in Haskell that can be used to represent only quantities
= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
thanks ... -deech

Am Freitag 08 Mai 2009 20:22:23 schrieb aditya siram:
Hi all, Is there a datatype in Haskell that can be used to represent only quantities
= 0? I got bitten by a bug because I forgot to reject an amount that was
below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
thanks ... -deech
I'm sure there are several implementations of a natural number datatype on Hackage (e.g. lazy Peano Numbers). And of course there are Word, Word32, Word64 (from Data.Word), but they wrap on underflow. Another option is to define an opaque type yourself: module Natural (Natural, mkNatural, maybeNatural) where newtype Natural = N Integer deriving (Eq, Ord, Show) mkNatural :: Integer -> Natural mkNatural n | n < 0 = error "Naturals must be non-negative" | otherwise = N n maybeNatural :: Integer -> Maybe Natural maybeNatural n | n < 0 = Nothing | otherwise = N n instance Num Natural where (N m) + (N n) = N (n+m) (N m) - (N n) = mkNatural (m-n) (N m) * (N n) = N (m*n) abs = id signum (N n) = if n == 0 then (N 0) else (N 1) negate n = error "Can't negate Naturals" fromInteger = mkNatural doesn't give you hard compile-time guarantees, but at least you get an error and not a hard-to-find bug.

That's an interesting question. I would like to see the answer too. I can think of a completely impractical way to do it: data Quantity = 0 | 1 | 2 | 3 | ... | 65532 But of course, listing every integer seems like a dumb solution. But this gives me more confidence that there is a smart solution to your problem and we just need to find it. Daniel. aditya siram wrote:
Hi all, Is there a datatype in Haskell that can be used to represent only quantities >= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
thanks ... -deech
------------------------------------------------------------------------
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

On Sat, May 9, 2009 at 2:24 AM, Daniel Carrera
That's an interesting question. I would like to see the answer too. I can think of a completely impractical way to do it:
data Quantity = 0 | 1 | 2 | 3 | ... | 65532
But of course, listing every integer seems like a dumb solution. But this gives me more confidence that there is a smart solution to your problem and we just need to find it.
Daniel.
What about operators? --- Ashok `ScriptDevil` Gautham

aditya siram wrote:
Hi all, Is there a datatype in Haskell that can be used to represent only quantities >= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
Maybe Word32 (or one of it's siblings) would do? It's basically the same as 'unsigned int' in C, so it can under- and over-flow. /M -- Magnus Therning (OpenPGP: 0xAB4DFBA4) magnus@therning.org Jabber: magnus@therning.org http://therning.org/magnus identi.ca|twitter: magthe

Cool, that's really interesting! So is it accurate to say "predicated"
datatypes [1] such as Int and String are provided by Haskell but you cannot
create them or specialize on a subset of them? And there are really only two
types of datatypes, tags [2] and the "predicated" types. Compound datatypes
are just a combination of the two.
-deech
[1] By predicated I mean a datatype that would actually cause a compiler
error ( not a runtime error ) if a method returned an out-of-bounds value.
[2] By tags I mean the data constructors, but I find it easier to think of
them as tags because they can appear alone, eg. data Coins = Penny | Nickel
| Dime | Quarter
where nothing is being constructed.
On Fri, May 8, 2009 at 5:06 PM, Magnus Therning
aditya siram wrote:
Hi all, Is there a datatype in Haskell that can be used to represent only quantities >= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
Maybe Word32 (or one of it's siblings) would do? It's basically the same as 'unsigned int' in C, so it can under- and over-flow.
/M
-- Magnus Therning (OpenPGP: 0xAB4DFBA4) magnus@therning.org Jabber: magnus@therning.org http://therning.org/magnus identi.ca|twitter: magthe
_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

2009/5/9 aditya siram
Cool, that's really interesting! So is it accurate to say "predicated" datatypes [1] such as Int and String are provided by Haskell but you cannot create them or specialize on a subset of them? And there are really only two types of datatypes, tags [2] and the "predicated" types. Compound datatypes are just a combination of the two.
-deech
[1] By predicated I mean a datatype that would actually cause a compiler error ( not a runtime error ) if a method returned an out-of-bounds value. [2] By tags I mean the data constructors, but I find it easier to think of them as tags because they can appear alone, eg. data Coins = Penny | Nickel | Dime | Quarter where nothing is being constructed.
I don't see where the "predicated datatype" differs from the tags type : Int could as well be implemented as a "data Int = 0 | 1 | 2 |..." (sparing consideration about characters authorized in a tag), String isn't primitive at all, in fact it's just a list of characters.... You can easily create them. To specialize on a subset of them is very easy too, you can use newtype or data and create a smart constructor, as well as appropriate instances. The only problem is that it is pretty hard to get compile time guarantee on some of them but no other classic language provides more guarantee : the only languages that can do better are those that have dependant types (Agda, Coq, Epigram...) and as you'll know if you tried them they're frequently harder to use than Haskell. NB : You can use Template Haskell to get some compile-time errors for the constants of your code. -- Jedaï

Magnus Therning wrote:
aditya siram wrote:
Hi all, Is there a datatype in Haskell that can be used to represent only quantities >= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
Maybe Word32 (or one of it's siblings) would do? It's basically the same as 'unsigned int' in C, so it can under- and over-flow.
What's under-flow?

Daniel Carrera wrote:
Magnus Therning wrote:
aditya siram wrote:
Hi all, Is there a datatype in Haskell that can be used to represent only quantities >= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
Maybe Word32 (or one of it's siblings) would do? It's basically the same as 'unsigned int' in C, so it can under- and over-flow.
What's under-flow?
Negative overflow:
let one = 1 :: Word8 one - 2 255
/M -- Magnus Therning (OpenPGP: 0xAB4DFBA4) magnus@therning.org Jabber: magnus@therning.org http://therning.org/magnus identi.ca|twitter: magthe

On Fri, May 8, 2009 at 11:22 AM, aditya siram
Hi all, Is there a datatype in Haskell that can be used to represent only quantities
= 0? I got bitten by a bug because I forgot to reject an amount that was below zero after applying a decrementing operator. A simple unit test would have caught this, but I was wondering if there was some way of getting the type system to ensure this.
thanks ... -deech
There are a number of ways of doing this, none of them entirely satisfactory. The essential problem is that subtraction becomes a partial function; i.e. if you try to subtract a and b, there's no way for the compiler to statically know if that's going to be nonnegative or not. One option would be to make a newtype of Integer, define (+), (*), etc. as with regular integers, define abs = id, negate = undefined. Then you can either make (-) a partial function (as in (NonNeg x) - (NonNeg y) = case x - y of z | z >= 0 -> z | otherwise -> undefined ) or leave subtraction undefined and make a maybeSubtract function that returns a Maybe value based on whether or not the result would be positive or negative. A third option would be to just take the absolute value of the result of a subtraction, although this should be used ONLY in situations where it is appropriate because usually you want to distinguish between x and -x. You could also use Peano numerals, but I don't think that those are very efficient. That's where you define data Nat = Zero | Succ Nat and so 3 :: Nat = Succ (Succ (Succ Zero)) etc. Hope that's of some help to you. Alex
participants (7)
-
aditya siram
-
Alexander Dunlap
-
Ashok Gautham
-
Chaddaï Fouché
-
Daniel Carrera
-
Daniel Fischer
-
Magnus Therning