2.3 KiB
Type Safe Variadic printf
module LessMacrosMoreTypes.Printf
%default total
While C can provide convenient string formatting by having hideously memory
unsafe variadics, and dynamic languages, like python, can do the same while
being memory safe by not being type safe, 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
the macro. We will explore this by implementing a simplified version of printf
in Idris from scratch.
This article is inspired by an exercise from chapter 6 of Type Driven Development with Idris, and is written as a literate Idris file, with the source available here.
Gameplan
Our goal is to provide a printf function that can be called, much like it's C equivalent:
Note
As this is a literate Idris document, and we haven't defined our
printffunction yet, we have to use afailingblock to ask the compiler to check that this code parses, and syntax highlight it for us, but not attempt to actually compile it.
failing
example_usage : String
example_usage = printf "%s %d %2d" "hello" 1 2
Parsing a Format String
First, we need a data structure to describe our format string. We define the
Format data type, with constructors for each of the format specifiers we will
be supporting, as well as a constructor to hold literal components.
data Format : Type where
||| A slot that should be filled in with a number
Number : (next : Format) -> Format
||| A slot that should be filled in with a number, padded to a certian number
||| of digits
PaddedNumber : (digits : Nat) -> Format
||| A slot that should be filled in with a string
Str : (next : Format) -> Format
||| A literal component of the format string that should not be interpolated
Literal : (literal : String) -> (next : Format) -> Format
||| The end of the format string
End : Format