Safe and Efficient printf in Idris: No Macros Required
2025-02-14
This article demonstrates how to implement a safe and efficient printf function in Idris without resorting to unsafe macros or variadics. By cleverly using type-level programming, the author parses the format string into a data structure and dynamically generates the function type signature based on it. This achieves the functionality of C's printf while maintaining memory and type safety. The article also explores handling runtime format strings and points out shortcomings of the implementation, such as unclear error messages, hinting at future improvements.
Development
Type-level Programming