Natural numbers in Haskell

19 Replies

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.

19 thoughts on “Natural numbers in Haskell”

  2. wren ng thornton

    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:

    limNatural :: a -> (Natural -> a) -> Natural -> a

    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.

    Like

    Reply ↓
    1. Wolfgang Jeltsch Post author

      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 a case 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.

      Like

      Reply ↓
      1. wren ng thornton

        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 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 (newtype of 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.

        Like

        Reply ↓
        1. Wolfgang Jeltsch Post author

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

          Like

          Reply ↓
          1. wren ng thornton

            The rules are for things like:

            • Moving the type casts associated with newtype un/wrappers out of the way of list and map fusion. This is unfortunately a sticking point with newtypes as they are currently implemented in GHC’s use of System Fc.
            • Fusing away the 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.
            • Removing other superfluous bounds checking (e.g., 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.

            Like

            Reply ↓
              1. wren ng thornton

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

                Like

                Reply ↓
          2. Henning

            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?

            Like

            Reply ↓

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

Leave a reply to wren ng thornton Cancel reply