Richard Feldman (Dec 01 2023 at 20:00): Richard Feldman (Dec 01 2023 at 20:00):a surprising benefit of the design where instead of having "number: \(num)" automatically call Num.toStr behind the scenes, we do "number: \(Num.toStr num)" explicitly - I just wrote some code that did \(Num.toStr num) in three strings in a row, at which point I of course immediately refactored it to call Num.toStr once and then reuse that string in all three places
Richard Feldman (Dec 01 2023 at 20:01):I've used a ton of languages where string interpolation works the other way, and it never occurred to me until just this moment how wasteful it is to create 3 duplicate strings from scratch to represent the same number :sweat_smile:
Brendan Hansknecht (Dec 01 2023 at 20:33):To be fair, I think in most languages they just generate the final string and don't build a temporary at all. They have a printf type function or format! type function that just builds the final string with ints as inputs.
Brendan Hansknecht (Dec 01 2023 at 20:33):So duplicate work to convert an int to a string, but no duplication in terms of storage or potential allocations etc
Jacob (Dec 02 2023 at 03:51):Lean does this.
IO.println s!"number: {num}
IO.println s!"Some number {some (2 + 3)}" -- "(some 5)"
would work or any type where an instance of ToString exists.
Jacob (Dec 02 2023 at 03:54):I think there is an optimization so its effectively the same as format
Jacob (Dec 02 2023 at 04:04):I remember testing if named expressions were only called ToString once and I'm pretty sure it was (re-used?).
EDIT: Nvm! Completely wasn't paying attention to what you were saying!
Last updated: Jul 06 2025 at 12:14 UTC