Type safe variadic printf

> in Idris

For a lower-tech approach, you can even do one in Standard ML[1,2], more or less in plain Hindley–Milner (no substantial use of modules). The error messages are admittedly miserable. Perhaps it would be more correct to call that one a type-safe middle ground between printf and std::ostream::operaror<<, though, and I have to admit that loses what for me is one of the principal advantages of (POSIX) printf: the format string is a string, so localization—which inevitably involves rearranging placeholders—is much easier.

It might be that the correct solution involves a string with placeholders, but with formatting instructions—and all dependencies on argument types—pushed outside (to the argument list or similar). I’ve toyed with something like that in C; unfortunately, it’s not as succint as normal printf unless I want to tie it to dynamic memory allocation. For C, there’s also the advantage that you can avoid pulling in floating-point formatting code if you don’t need it, without resorting to GCC-specific tricks like Cosmopolitan does[3], and that code is the biggest (code and data) space hog that keeps printf out of embedded and other kinds of lean programs.

[1] http://mlton.org/Printf

[2] http://mlton.org/Fold

[3] https://justine.lol/sizetricks/

Not to fully encapture C's variadic printf, but on the macro front, I've been having fun creating type checking for macros by a constexpr allocation from a _generic switch type check of the args and then checking the result with static_asserts. I think there was a hack before as you mentioned but would have to dig through my tests to find it, but the C23 version is quite clean. Might want see if I can get it to be clean for a variadic printf version.

If you have type checking but not named arguments, it provides a fair degree of sanity checking.

And as much as named arguments are nice from a user perspective, they do have significant runtime overhead if the format string can be localized.