JacquesCarette
`Expr`'s `exactDbl`: Should we really have it?
See https://github.com/JacquesCarette/Drasil/issues/3986#issuecomment-2529682741 for 'what to do' information.
Original Description: exactDbl is a constructor for Expr, Literal, etc. that lets us define a (whole) real number and present it (when rendered) as a whole number without the decimal places. Is this really something we want? I remember @JacquesCarette previously mentioning an intermixing of display knowledge with actual knowledge, and I think this is one such case. Rendering 1.0 as 1 could be left as a configuration option should we choose to remove exactDbl.
I'm not entirely sure of the question, but if you are asking do we sometimes want to display 1 and other times 1.0 in the same document, then the answer is yes. I don't really think of it as a display option, definitely not a global configuration where all 1s would be 1 or 1.0. Whether it is 1 or 1.0 is depends on the case. If we have one of something, like one projectile, we don't really want to ever say we have 1.0 projectiles. In the derivation of some equations we end up with terms like 1/pi. The 1 really does mean 1 and again, 1.0/pi isn't right.
I'm not sure I answered your question. :smile:
Thank you, @smiths! It sounds like understood the question -- I just phrased it poorly.
I have a follow-up question: What is our criteria for using exactDbl? Is there anyway that we can have the choice to present a ~~(real)~~ number with $X.Y$, $X$ (if $Y is \bar{0}$), or $X \frac{a}{b}$ (amongst the many other possible forms) automatically made for us? Does it depend on the type, the unit, or both?
@balacij I would think we could capture this with the type information. I think we currently use double for everything. Some of our doubles are really better thought of as natural numbers. Natural numbers don't have a fractional part. If we knew the type, we could display it properly. I think there are cases where it is a real number, but still exactly equal to 1, like in a derivation where we end up with a literal 1 because of cancellation (or some other reason). Maybe we need a different type for that? We should know when we are building our theory if we want something to be exactly 1, either as a natural number or real. I'm sure @JacquesCarette has some thoughts on this. :smile:
exactDbl is an awful name. Some times we have an exact quantity, i.e. with no 'approximation' at all, that we nevertheless want to use seamlessly in a context where we have reals (and even doubles).
We should take a look at all uses of exactDbl to see if they all "mean the same thing", and then maybe change its name to something more semantic.
