It is a bit surprising that Haskell has no type for natural numbers. The Haskell Report defines only Integer for, well, integers and Int for integers that are reasonably small. The base package then adds Word as the unsigned variant of Int as well as types for signed and unsigned integers with a fixed number of bits. An unsigned variant of Integer is missing.
That is why I recently wrote the natural-numbers package. It defines a type Natural as a simple wrapper around Integer. Negative numbers are avoided by checks, which are only performed where a negative number can actually occur. So performance should be quite good, although I have not done any tests in this direction.
Surprisingly, nobody seems to have published such a package on HackageDB before. The naturals package is pretty close to what I have written. However, its Natural type covers a so-called indeterminate value. This value is used where negative numbers would occur usually. For example, it is the result of the expression 3 - 4. I think this is not reasonable, since that indeterminate value is not a natural, while being a value of type Natural. So the natural-numbers package I have developed always raises an error if an operation cannot be performed.
There are further packages on HackageDB that deal with natural numbers, but these have goals different from mine. The nat package has a natural number implementation that employs lazyness, while the packages type-level-natural-number, natural-number, and type-unary deal with type-level representations of natural numbers.
The advantage of using an indeterminate/failure value is that you can avoid partial functions and runtime crashes, as long as you avoid using
fromIntegralto go fromNaturalto, say,Int. In your version, any arithmetic operation can result in a crash.Well, if you don’t want your program to crash, you should check that your natural number computations will succeed.
If you don’t do this, you’ll get a crash with my package, but with indeterminate values, you’ll risk that your program silently does something wrong.
This does not mean that failure values are bad as such. But it should be explicit in the types that you have them. If you use
Maybe Naturalinstead ofNatural, it is obvious that there is a special value (Nothing) for signaling errors. Including the failure value into theNaturaltype, however, pretends that failure is a natural, so to say.The use of an indeterminate value also breaks certain properties. For example, an instance of
Numshould obey the constraint∀
n,m,k.(n - m) + k=(n + m) - k.This cannot hold for natural numbers, independently of whether there is an indeterminate value or not. However without an indeterminate value, we have at least a slightly weaker property.
Let ⊑ denote the information order. That is, let a ⊑ b mean that a and b are equal, or a is less defined than b. In particular, this means that ⊥ ⊑ b for any b. Without an indeterminate value, we have at least the property
∀
n,m,k.(n - m) + k⊑(n + k) - m.With an indeterminate value, we do not enjoy such a property, since
Indeterminate⊑nholds for no natural number
n.In general without an indeterminate value, we might not enjoy a desired equality L = R, but we usually still enjoy the condition
L ⊑ R ∨ R ⊑ L .
The presence of an indeterminate value usually destroy this.
I think the actual problem with naturals and the
Numclass is thatNumis already too feature-rich. There should probably be a superclass ofNum, which doesn’t contain(-)andnegate.There should definitely be a superclass of
Numfor semirings (you’ll want to get rid ofabstoo, along with subtraction and negation).Sorry for the critic, but the simple reason why there is no such package on hackage is that it brings nothing.
As you just wrote, “you should check that your natural number computations will succeed”, therefore your new
Naturaltype is pointless. I can already check that myIntegercomputations will eventually give a number ≥ 0, no need for a new package.Even worse, with
IntegerI can perfectly have not natural intermediate binded values and still have a natural result. Think of3 - 5 + 6which is a perfectly valid expression of aNaturalbut will crash with your library.A
Naturaltype would make sens if it allowed the compiler to provide more guarantees, but at the moment that would require dependant types.A
Naturalcan be used in function types to specify pre- and postconditions. For example, thelengthfunction could haveNaturalas its result type, so that the user has a static guarantee that its result will never be negative. On the other hand, thetakefunction could have typeNatural -> [el] -> [el],so that the implementation of
takewould not need to check if its argument is negative. The types would then make it easy to see that an expressiontake (length list1) list2is safe.
If all operations on
Naturalwere total, you would only have to check manually that all conversions fromIntegertoNaturalare safe. Unfortunately, there are(-)andnegate, which are not total. That is why I think that theNumclass is too feature-rich, andNaturalshould be an instance only of some semiring class or similar. If integer literals (without a leading minus sign) would then be defined in terms of this new class, the situation would be close to perfect.Until the situation is not like this, you can avoid using
(-)andnegateforNatural. This is still a bit better than usingInteger. WithInteger, you cannot be sure to have a non-negative number even when avoiding(-)andnegate, as you could have received a negativeIntegerfrom somewhere else.wow! great idea and simple source code which was very easy to understand. thank you for that nice library
I have a similar newtype in some as-yet-unpublished code, which I have considered strongly from the optimization perspective. However, my version uses saturating subtraction (aka “monus”) rather than partial subtraction or indeterminate values.
One function I’ve found to be quite helpful in writing code using natural numbers is presenting a view as if the natural numbers were constructed via Peano encoding:
This is especially helpful since there are so many reasons to check for zero before doing things (e.g., taking the predecessor), so you might as well provide it directly.
I probably should add an operator for saturating substraction too. Do you know a nice operator name for it?
In what way is your implementation of naturals different from mine, especially with respect to optimization?
Your
limNaturalfunction is acutally acaseor eliminator for natural numbers, as it takes continuations for the two alternatives (zero, non-zero) as arguments. An implementation of views would be more like what has been done for sequences. Do you think this should be done for naturals also?I also wonder whether it is reasonable to implement a fold for natural numbers.
That should be
elimNatural, and yes, it’s just the elimination form / case analysis (hence the name). I think it still qualifies for being called a “view”, since it’s actually case elimination for the Peano data type, rather than for the flat representation of natural numbers, or the binary representation, or … I’ve just optimized away theMaybe, which is the data type version of the view. As mentioned in the documentation, if you want the datatype version you can just doelimNatural Nothing Just.My point was that providing it allows us to keep the type abstract (which helps in preserving the lack of indeterminate values), and yet still have an efficient elimination. The big thing is that this gives a safe version of
pred, and code for natural numbers is often using a lot ofsuccandpred. Now that I think of it, this is also just a CPSed version of subtracting; so I should offer a more general elimination which lets you CPS the subtraction of any number.For the
Naturaltype there really isn’t a whole lot of optimization you can do; mostly just eliminating redundant safety checks and providing decent error messages. Though I do have a bunch of rewrite rules and inlining pragma, so that we don’t lose the ones fromInteger. I also have aNattype (newtypeofInt) which has more room for optimization since you have to deal with saturation at the upper bound too.I don’t know of any decent non-unicode symbols for monus. The most common symbol I’ve seen in mathematics is a subtraction symbol with a dot above it. Of course, using a dotted name like
.-or-.would collide with the standard use of dotted names for vector/matrix ops. I’ve seen some Haskell libraries use|-or-|for monus, but I forget which.I’ve added a view function to my library now. It converts a natural to a value of a dedicated type
I’ve also added a monus operator, just called
View, which is isomorphic toMaybe Natural. I hope GHC will be clever enough itself to optimize away theView.monusat the moment, and a fold operator.Do you really need rewrite rules and inline pragmas? I hoped that GHC would do sensible inlining automatically and use the rewrite rules for
Integerwhen working withNatural.The rules are for things like:
newtypeun/wrappers out of the way of list and map fusion. This is unfortunately a sticking point withnewtypes as they are currently implemented in GHC’s use of System Fc.toNaturalandfromNaturalconversions (e.g.,fromNatural . toNaturalboils down to the non-negativity check, andtoNatural . fromNaturalis just the identity function). I actually have a few different functions fortoNatural(unsafe doesn’t check; unsafe throws an exception; safe returnsMaybe) so all of those are handled here.pred . succis also the identity function; whereassucc . predis just the non-zero check).Some of the other rules (e.g., semiring laws regarding
0and1, or special casing thefromIntegralclass method based on types) are probably superfluous. But I don’t have a large enough test corpus of code to legitimately check whether they (a) fire much, or (b) actually affect performance significantly.I’ve released a new version, which contains some rewrite rules.
I don’t understand your first point, regarding list and map fusion. Could you maybe elaborate?
Consider the case where you have a list (or other Functor) of Naturals and you want to convert them to a list of Integers (or vice versa in the cases where you can demonstrate safety). The naive approach is just to use
map fromNatural; however, that requires traversing the list to do essentially nothing. List fusion will be able to remove this when it occurs in pipeline with other functions, so you get thatmap f . map fromNatural . map g⟹map (f . fromNatural . g)which is great. However, after all the fusion is done you may still be left with some calls tomap fromNatural, which we’d like to replace by a constant-time type coercion—which is guaranteed to be safe for the case of newtypes. Hence, a rule formap fromNatural = unsafeCoercewhich is essentially the same as the standard rule:map id = id.The problem arises, however, that
unsafeCoercegets in the way of other rules and optimizations firing. Thus, we want various rules to moveunsafeCoerceout of the way whenever we can.Is there a library on HackageDB (not necessarily related to natural numbers) which contains such rewrite rules, so that I could have a look at them?
Thank you very much for this library. I would like to use the given view but since the data constructors of
Vieware not exported that’s not possible. Is there any reason why you don’t export them?No, I had just forgotten to export them. This is fixed in the new version I’ve just uploaded.
Thank you very much.
I needed this library too, when I was doing bindings for base types in Agda. My version is at https://github.com/agda/agda-data-bindings/blob/master/src/Data/Natural/AgdaFFI.hs. It looks a lot like yours, but I made all the functions total, with truncating semantics, so
fromIntegerof a negative number is zero. I didn’t include any rewrite rules.[...] Haskell does not come with a type for natural numbers, we make use of the natural-numbers [...]