Supporting the rationals

#1

Currently Dhall has a lot of support for Natural numbers - witnessing the total order, addition and truncated subtraction. There is also support for Integer and Double, but both of these are essentially just literals, with some basic support to turn them into other types, but they cannot be operated on. I’d like to propose we introduce some support for rational numbers.

The project I’m exploring at the moment is moving the pricing modelling in CircuitHub into Dhall. Essentially the pricing system can be modeled as an extraction phase to collect some features, and then these features are fed into the pricing model to provide prices at various quantities and lead times. The model is sensitive to features such as the dimensions of your circuit board, which can be represented as either Naturals that represent our smallest unit (let’s say micrometers), or we could use exact rationals that represent the number in meters. A similar scenario crops up with the actual price itself. The price of something could be an exact rational, or we could use a lossy encoding of some kind of base unit (say 1/100th of a US cent).

(Positive) rationals can currently be modeled by the type { numerator : Natural, denominator : Natural }, but they are painful to construct as literals. I would like to be able to write things such as Rational/le features.board-width 0.3 to encode the condition “the board width is under 0.3m”. Currently this has to be written as Rational/le features.board-width (cm 30) (or mm 30000, etc), which is obscuring the translation of constraints as delivered to us by our third-party manufacturers. I’d like the code to read as close to the original specification as possible.

As for what should change, I’m less clear. From my side, I would like to be able to witnessing the total ordering on rationals, and constructing them from decimal numbers. I don’t think I’ve yet needed negative rationals, only positive.

1 Like
#2

Recapping from the discussion in https://github.com/dhall-lang/dhall-lang/pull/675, I think if we add support for Rationals they should be a first-class language feature (i.e. the language should, at a minimum, have a Rational type, literals, and any sensible conversion functions). My reasoning is that Dhall should have an ergonomic way to losslessly represent these types of numbers as a configuration file format.

I’m still dragging my feet a bit on implementing more arithmetic in Dhall, but I’ll still try to take this idea as far as I can.

I think it makes sense for Rational numbers to have a syntax separate from Doubles and I’ll propose the syntax m / n where m is an Integer and n is a Natural. Note that we would allow n = 0 because we don’t (yet) attempt to do any Natural arithmetic or simplifications. It would basically just be a compact version of { numerator : Integer, denominator : Natural }.

I think it would also make sense to add the following built-in:

Double/toRational : Double → Rational

… where:

Double/toRational 0.3 = 3 / 10

Double/toRational 1e100 = 10000…000 / 1  -- Yes, we would expand it out

Double/toRational 0.0 = +0 / 1

Double/toRational -0.0 = +0 / 1  -- Dhall doesn't distinguish `+0` and `-0`

Double/toRational Infinity = +1 / 0

Double/toRational -Infinity = -1 / 0

Double/toRational NaN = +0 / 0

Then if we provide a built-in to extract the numerator and denominator you can almost compare Rational numbers:

Rational/toRecord : Rational → { numerator : Integer, denominator : Natural }

The main thing you’re missing is Integer arithmetic. If you had the ability to multiply and compare Integers then that would give the ability to compare Rationals, like this:

let Rational/lessThan : Rational → Rational → Bool
      = λ(x : Rational)
      → λ(y : Rational)
      → let rX = Rational/toRecord x

        let rY = Rational/toRecord y

        in  Integer/lessThan
              (rX.numerator * Natural/toInteger rY.denominator)
              (rY.numerator * Natural/toInteger rX.denominator)

in  Rational/lessThan
#3

Did you mean to say this? We support addition, truncated subtraction and multiplication on Naturals. Perhaps you meant Integer arithmetic?

Yea, I already have a reasonable library for Rationals built on pairs of Naturals (product/sum/ordering) - built in exactly the way you are suggesting.

#4

So I’ve been thinking about this some more and I think adding support for +/* for Integers is fairly non-controversial. Since Dhall has no type inference and the operators are built-in we have the luxury of overloading their behavior to work on different types.

I think the remaining thing is providing built-ins that can power Integer/lessThan. We could do something similar to what we did for Naturals (i.e. implement an Integer/subtract and also an Integer/positive)

#5

I think if we end up with first-class Rational (the use case for which seems light to me, since it’s basically just lightweight syntax for a record?) I think banning denominators of 0 is super important even if we don’t allow arithmetic or simplifications, since a denominator of 0 is decidedly not a Rational number.

1 Like
#6

Some thoughts on this:

  1. New syntax x / y to construct the rational number x/y as a record type: { numerator = x, predenominator = y - 1} (names subject to bike shedding). This constructively rules out x/0. Should x / y syntax allow arbitrary expressions for x and y though? If so, how do we reject x / (Natural/subtract 2 1) which normalises to x / 0?
  2. The builtin Double/toRational that takes any double literal and turns it into a record of the aforementioned type. But we need to reject Double/toRational NaN - how would we do that? It’s even more complicated if we have Double/toRational x where x is free - how do we make progress on this?
#7

@ocharles: My proposal is that x / y is not a synonym for a record (i.e. you have to explicitly convert it to a record using Rational/toRecord). Because it is a not a record, x and y must be Integer/Natural literals, respectively and cannot be abstract variables.

In other words, this would not be valid (and would be a syntax error):

let x = +1

let y = 1

in  x / y

So if we require y to be a Natural literal, then we can rule out 0 syntactically.

That said, I’d personally prefer to permit 0, if only so that Double/toRational can return 0 denominators for NaN/Infinity/-Infinity

#8

Wouldn’t it be nicer to have Double/toRational with type Double -> Optional Rational then? Permitting 0 as a denominator would make arithmetic with rationals more tricky, I believe.

I also wonder whether we should restrict our Rational type to represent non-negative rational numbers (which apparently would be enough for @ocharles’ needs). Signedness seems easier to add than to take away. Alternatively we could have a type parameter for the type of the numerator, and have operations for both Rational Integer and Rational Natural.

#9

@sjakobi: What arithmetic on Rationals would fail with 0 denominators?

#10

Yeah, maybe arithmetic wouldn’t be the problem. But with a 0 denominator you still have an invalid rational number, and so far Dhall seems to have tried to keep states like that unrepresentable.

#11

@sjakobi: Dhall strives to be total, meaning that every function produces a sensible output. As long as we don’t try to evaluate 1 / 0 (i.e. it is inert, like the equivalent record) then I don’t see an issue.

That said, I’m still trying to hold off on adding more arithmetic in general, so I’m not going to push on this too strongly :slight_smile:

1 Like
#12

Well, I assume that even if we don’t evaluate 1 / 0 in Dhall, that number will end up being evaluated somewhere and at that point raise the question of what do about a 0 denominator.

#13

Right, my problem is about working with either money or physical measurements (in fact, both - the cost of something is proportional to it’s area). For this case, I am only interested in finite positive rationals.

#14

Ah, good point. I totally forgot about marshaling the value into the host language. Never mind, then :slight_smile:

#15

Money shouldn’t need rationals, right? Or do you have a specific use case for sub-subunit values?

#16

When working with money you want absolute precision until the end, in which case you truncate to fixed precision (either in your favour or the customers favour)

3 Likes
#17

Has there been additional thoughts on including rationals in Dhall? I have a similar challenge as ocharles, where I need to verify that some physical values that would be nice to type check are in a bound (using the asserts) and to have the right precision until the end.

#18

How would one implement the function

Double/toRational 0.3 = 3 / 10

?

As I understand, there is not enough information to do that!

#19

I have implemented some common functions at https://github.com/sjakobi/dhall-rational.

$ dhall repl
Welcome to the Dhall v1.29.0 REPL! Type :help for more information.
⊢ :let Rational = https://raw.githubusercontent.com/sjakobi/dhall-rational/a39661197da71e7bd361d4cdda6023aaff93f8a5/package.dhall

<snip>

⊢ :let a = Rational.unsafeRational +4 3

a : { numerator : Integer, predenominator : Natural }

⊢ :let b = Rational.e +2 -3

b : { numerator : Integer, predenominator : Natural }

⊢ Rational.show (Rational.multiply a b)

"+8/3000"

⊢ Rational.lessThanEqual a b

False

I think some builtin support for division and operations like GCD would be helpful, but might not be strictly required depending on what you want to do.

@vmchale Indeed Doubles are currently completely opaque.

1 Like
#20

I think the idea here is not to implement a Double/toRational function but just use rationals directly. At least my use case would stay within using rationals only.