The Type of Sprintf - Ryan Brewer

Today I decided to write a little post about giving a type to the sprintf function via dependent types. The idea of this and related functions (like printf) is to have the first argument be a string, and special patterns in the string determine what the following arguments should be. For example:

For languages that have compile-time (aka "static") types, this function generally has to be a special case in the typechecker. There's no way for the user to create a function that does something similar, since the type of the function depends on the contents of the format string. You generally couldn't even do something like this:

However, in a dependent type system, we actually do have the power to make functions like these. In fact, sprintf is sometimes given as the main example of what dependent types allow you to do that you couldn't do with only refinement types. For full transparency, I got this example from the lecture notes of Daniel Gratzer. Hopefully this blog post makes a cool example a little more accessible.

Without further ado, the set-up goes like this. As you can imagine, we have to parse the format string at compile-time to determine the types of the arguments. Therefore we'll start by making a simple Token datatype:

Leave a Comment