Dealing with negative numbers

#1

With apologies if it’s been discussed before, but I didn’t see anything.

What’s the rational behind having no support for negative numbers (i.e. Integers can be negative, but are opaque)? I’ve been using Dhall extensively for templating text with dhall text, but a sort of very basic thing one frequently wants to do is treat a value differently if it’s greater or less than zero (e.g. print negative number in red and positive in black). Since there’s no comparison for Integers nor even an Integer/isNegative or some such thing, this necessitates a lot of boilerplate, with a bunch of values that are just integers (and should ideally be represented in Json as such) having to instead be written as either:

< Positive : Natural | Negative : Natural>

or as something like

{ value : Natural, negative : Bool }

Both of these are cumbersome to actually use, since they necessarily require writing something like cost = MyType.Negative 5 rather than just cost = -5 and clutter things if/when they get turned to Json. Not to mention that there is the issue of having both “positive” and “negative” zero.

Is there a compelling reason to avoid arithmetic or at least sign checking for Integer? Or is there a better way of responding to negative values that I’m just overlooking (which is entirely possible)?

#2

@SiriusStarr: There’s no particular reason we omitted it. We omit operations by default and then add built-ins based on user request.

A couple of previous threads have brought up a potential Integer/toNatural built-in or something similar:

https://discourse.dhall-lang.org/search?q=Integer%20Natural

The main issue with the proposals for that built-in so far is that they result in an awkward type if you want to make invalid states unrepresentable. For example, if you choose a type like this:

Integer/toNatural : Integer → < Negative : Natural | Zero | Positive : Natural >

… then you either have to use Negative 0 to mean -1 (which is awkward) or you have to deal with Negative 0/Zero/Positive 0 meaning the same thing.

Rather than bless a particular representation, I’ve been trying to think about how to decompose that built-in into smaller built-ins that have only one ambiguous type, and the built-ins that I might suggest are:

Integer/negate : Integer → Integer

Integer/truncate : Integer → Natural  -- Truncates to zero for negative numbers

Then with those two built-ins, plus Natural/isZero you can convert an Integer to any representation that works best for you.

Here are some example utilities you could build on top of those:

let Integer/nonPositive
      : Integer → Bool
      = λ(n : Integer) → Natural/isZero (Integer/truncate n)

let Integer/positive
      : Integer → Bool
      = λ(n : Integer) → Integer/nonPositive n == False

let Integer/nonNegative
      : Integer → Bool
      = λ(n : Integer) → Natural/isZero (Integer/truncate (Integer/negate n))

let Integer/negative
      : Integer → Bool
      = λ(n : Integer) → Integer/nonNegative n == False

let Integer/toNatural : Integer → Optional Natural
      =   λ(n : Integer)
        → if Integer/negative n
          then None Natural
          else Some (Integer/truncate n)
2 Likes
#3

These seem like good, minimal built-ins that would allow for all the necessary implementations. Unclear if truncate would be the best name though since it’s a common function already in most languages for converting floating point to integers, which could possibly be confusing? Off the top of my head, perhaps something like clampPositive / clampNonNegative or maxZero / maxWithZero might be less ambiguous names that directly imply that negatives become zero. Probably better ideas out there, just iterating on it.

Those two built-ins would also allow absolute value in addition to the ones you provided, another useful thing:

let Integer/abs
    : Integer → Natural
    =   λ(n : Integer)
      →       if Integer/negative n
        
        then  Integer/truncate (Integer/negate n)
        
        else  Integer/truncate n
#4

How about Integer/toNatural : Integer -> Natural for the truncating conversion?

That would be somewhat consistent with Natural/subtract where we also didn’t mention the truncation in the name.

#5

My only concern with Integer/toNatural is I don’t believe any of the other type conversions (e.g. Integer/toDouble or Natural/toInteger or Optional/toList) are “lossy.” (Correct me if I’m wrong, obviously.) I personally would rather see the Integer/toNatural : Integer → Optional Natural presented above for a toNatural function, since that is explicit about its potential to fail, rather than “failing” silently by truncating to zero.

To be fair, that (Integer/toNatural : Integer -> Optional Natural) COULD be used as the built-in instead of the proposed Integer/truncate, since it can be defined in terms of it.

let Integer/truncate
    : Integer → Natural
    = λ(n : Integer) → Optional/default Natural 0 (Integer/toNatural n)

But the truncate option is arguably the more “low-level”/simple built-in and thus potentially the better choice.

#6

What I don’t like so much about the Integer/truncate name is that there’s no indication that the result is a Natural.

Integer/toNatural : Integer -> Optional Natural seems fine to me. isZero, positive, negative could all be implemented very easily with it.

#7

Or how about Integer/truncateToNatural : Integer -> Natural? That’s admittedly a bit long but IMHO very easy to understand.

#8

For the Optional version, how about Integer/clamp : Integer → Optional Natural?

#9

Sorry, I mis-spoke. I meant to propose to use Integer/clamp for the non-optional builtin:

Integer/clamp : Integer → Natural
#10

I think Integer/clamp is definitely fine, or Integer/clampToNatural if we want to be more explicit about the type conversion.

#11

Now that I’ve looked up what clamp means, it seems quite fitting. IMHO Integer/clampToNatural is slightly better than Integer/clamp because it mentions the conversion.

#12

Just a small comment on this part – it should already be possible to convert this type to an Integer at the end of your pipeline so that the host language and/or JSON conversion only see an Integer and not your union type.

#13

What do you mean? The only builtin that produces Integers is Natural/toInteger, which can only produce non-negative Integers…

#14

IMHO Integer/negate and Integer/clampToNatural are ready to be standardized.

@SiriusStarr would you like to do this yourself?

#15

I’ll take a stab at it; will be good practice.

1 Like
#16

PR #780 up. Someone smarter than I please confirm the beta-normalization for Integer/negate, haha.

1 Like