Get the latest tech news
Type safe variadic printf
While C can provide "convenient" string formatting by having hideously unsafe variadics, and dynamic languages, like python, can do the same, many type safe languages, such as Rust, are forced to provide such functionality through the use of a macro. Dependently typed languages, like Idris, can provide a printf like formatting interface, while maintaining both memory and type safety, without the need for macros. We will explore this by implementing a simplified version of printf in Idris from scratch.
The specifics of the parsing aren't really material to the main point of this article, but we use a basic pattern matching approach, calling into our helper functions as appropriate. Being fully honest, I'm not entirely sure what use cases this particular function would make sense for, but it provides a first taste of working with type signatures that depend on values that aren't known until runtime, which is a concept we will expand upon in future entries in this series. Avoiding using a macro also gives us a lot of neat bonuses, like printf automatically playing nice with partial application and currying, with no extra effort on our part.
Or read this on Hacker News