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
fromIntegral
to go fromNatural
to, say,Int
. In your version, any arithmetic operation can result in a crash.LikeLike
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 Natural
instead ofNatural
, it is obvious that there is a special value (Nothing
) for signaling errors. Including the failure value into theNatural
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 ⊑ 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
⊑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 condition
L ⊑ R ∨ R ⊑ L .
The presence of an indeterminate value usually destroy this.
I think the actual problem with naturals and the
Num
class is thatNum
is already too feature-rich. There should probably be a superclass ofNum
, which doesn’t contain(-)
andnegate
.LikeLike
There should definitely be a superclass of
Num
for semirings (you’ll want to get rid ofabs
too, along with subtraction and negation).LikeLike
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
Natural
type is pointless. I can already check that myInteger
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 of3 - 5 + 6
which is a perfectly valid expression of aNatural
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
A
Natural
can be used in function types to specify pre- and postconditions. For example, thelength
function could haveNatural
as its result type, so that the user has a static guarantee that its result will never be negative. On the other hand, thetake
function could have typeNatural -> [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 expressiontake (length list1) list2
is safe.
If all operations on
Natural
were total, you would only have to check manually that all conversions fromInteger
toNatural
are safe. Unfortunately, there are(-)
andnegate
, which are not total. That is why I think that theNum
class is too feature-rich, andNatural
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
(-)
andnegate
forNatural
. 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 negativeInteger
from somewhere else.LikeLike
wow! great idea and simple source code which was very easy to understand. thank you for that nice library 🙂
LikeLike
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.
LikeLike
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
limNatural
function is acutally acase
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?I also wonder whether it is reasonable to implement a fold for natural numbers.
LikeLike
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 ofsucc
andpred
. 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 fromInteger
. I also have aNat
type (newtype
ofInt
) 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
I’ve added a view function to my library now. It converts a natural to a value of a dedicated type
View
, which is isomorphic toMaybe Natural
. I hope GHC will be clever enough itself to optimize away theView
. 😉 I’ve also added a monus operator, just calledmonus
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 withNatural
.LikeLike
The rules are for things like:
newtype
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.toNatural
andfromNatural
conversions (e.g.,fromNatural . toNatural
boils down to the non-negativity check, andtoNatural . fromNatural
is 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 . succ
is also the identity function; whereassucc . pred
is just the non-zero check).Some of the other rules (e.g., semiring laws regarding
0
and1
, or special casing thefromIntegral
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
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?
LikeLike
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 = 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 moveunsafeCoerce
out of the way whenever we can.LikeLike
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?
LikeLike
Thank 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
No, I had just forgotten to export them. This is fixed in the new version I’ve just uploaded.
LikeLike
Thank you very much.
LikeLike
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
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