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