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.

hesselinkThe advantage of using an indeterminate/failure value is that you can avoid partial functions and runtime crashes, as long as you avoid using

`fromIntegral`

to go from`Natural`

to, say,`Int`

. In your version, any arithmetic operation can result in a crash.LikeLike

Wolfgang JeltschPost authorWell, 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 Natural`

instead of`Natural`

, it is obvious that there is a special value (`Nothing`

) for signaling errors. Including the failure value into the`Natural`

type, 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

`Num`

should 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⊑bmean thataandbare equal, orais less defined thanb. In particular, this means that ⊥ ⊑bfor anyb. 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`

⊑`n`

holds 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 conditionL⊑R∨R⊑L.The presence of an indeterminate value usually destroy this.

I think the actual problem with naturals and the

`Num`

class is that`Num`

is already too feature-rich. There should probably be a superclass of`Num`

, which doesn’t contain`(-)`

and`negate`

.LikeLike

wren ng thorntonThere should definitely be a superclass of

`Num`

for semirings (you’ll want to get rid of`abs`

too, along with subtraction and negation).LikeLike

Paul RivierSorry 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

`Natural`

type is pointless. I can already check that my`Integer`

computations will eventually give a number ≥ 0, no need for a new package.Even worse, with

`Integer`

I can perfectly have not natural intermediate binded values and still have a natural result. Think of`3 - 5 + 6`

which is a perfectly valid expression of a`Natural`

but will crash with your library.A

`Natural`

type would make sens if it allowed the compiler to provide more guarantees, but at the moment that would require dependant types.LikeLike

Wolfgang JeltschPost authorA

`Natural`

can be used in function types to specify pre- and postconditions. For example, the`length`

function could have`Natural`

as its result type, so that the user has a static guarantee that its result will never be negative. On the other hand, the`take`

function could have type`Natural -> [el] -> [el]`

,so that the implementation of

`take`

would not need to check if its argument is negative. The types would then make it easy to see that an expression`take (length list1) list2`

is safe.

If all operations on

`Natural`

were total, you would only have to check manually that all conversions from`Integer`

to`Natural`

are safe. Unfortunately, there are`(-)`

and`negate`

, which are not total. That is why I think that the`Num`

class is too feature-rich, and`Natural`

should 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

`(-)`

and`negate`

for`Natural`

. This is still a bit better than using`Integer`

. With`Integer`

, you cannot be sure to have a non-negative number even when avoiding`(-)`

and`negate`

, as you could have received a negative`Integer`

from somewhere else.LikeLike

mekeorwow! great idea and simple source code which was very easy to understand. thank you for that nice library 🙂

LikeLike

wren ng thorntonI 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.

LikeLike

Wolfgang JeltschPost authorI 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

`limNatural`

function is acutally a

or 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?caseI also wonder whether it is reasonable to implement a fold for natural numbers.

LikeLike

wren ng thorntonThat 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 the`Maybe`

, which is the data type version of the view. As mentioned in the documentation, if you want the datatype version you can just do`elimNatural 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 of`succ`

and`pred`

. 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

`Natural`

type 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 from`Integer`

. I also have a`Nat`

type (

ofnewtype`Int`

) 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.LikeLike

Wolfgang JeltschPost authorI’ve added a view function to my library now. It converts a natural to a value of a dedicated type

`View`

, which is isomorphic to`Maybe Natural`

. I hope GHC will be clever enough itself to optimize away the`View`

. 😉 I’ve also added a monus operator, just called`monus`

at 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

`Integer`

when working with`Natural`

.LikeLike

wren ng thorntonThe rules are for things like:

un/wrappers out of the way of list and map fusion. This is unfortunately a sticking point withnewtype

s as they are currently implemented in GHC’s use of System Fc.newtype`toNatural`

and`fromNatural`

conversions (e.g.,`fromNatural . toNatural`

boils down to the non-negativity check, and`toNatural . fromNatural`

is just the identity function). I actually have a few different functions for`toNatural`

(unsafe doesn’t check; unsafe throws an exception; safe returns`Maybe`

) so all of those are handled here.`pred . succ`

is also the identity function; whereas`succ . pred`

is just the non-zero check).Some of the other rules (e.g., semiring laws regarding

`0`

and`1`

, or special casing the`fromIntegral`

class 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.LikeLike

Wolfgang JeltschPost authorI’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?

LikeLike

wren ng thorntonConsider 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 that`map 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 to`map 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 for`map fromNatural = unsafeCoerce`

which is essentially the same as the standard rule:`map id = id`

.The problem arises, however, that

`unsafeCoerce`

gets in the way of other rules and optimizations firing. Thus, we want various rules to move`unsafeCoerce`

out of the way whenever we can.LikeLike

Wolfgang JeltschPost authorIs 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?

LikeLike

HenningThank you very much for this library. I would like to use the given view but since the data constructors of

`View`

are not exported that’s not possible. Is there any reason why you don’t export them?LikeLike

Wolfgang JeltschPost authorNo, I had just forgotten to export them. This is fixed in the new version I’ve just uploaded.

LikeLike

HenningThank you very much.

LikeLike

asajeffreyI 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

`fromInteger`

of a negative number is zero. I didn’t include any rewrite rules.LikeLike

Pingback: Dependently typed programming and theorem proving in Haskell « Wolfgang Jeltsch