Skip to main content

Posts

Showing posts from November, 2016

Dependently-typed Curried printf in C++

Just a few days ago I came across an intriguing blog-post about type-safe printf using dependent typing. The blog-post has since become inaccessible and therefore, I've copied an excerpt here. I want to thank Zesen Qian for publishing this blog-post.

.... printf originated from the C programming language and has been a headache since then because a proper call of printf requires the number and types of arguments to match the format string; otherwise, it may visit a wild memory or a wrong register. In recent versions of GCC this issue is addressed by type checks hard coded into the compiler itself, which is ugly because the compiler should not be caring about the safety of applications of a specific function....

The key issue here is that, considering the curried version, the type of the returned function of applying the format string to printf, actually depends on the value of that format string. That is to say, printf "%s" : String -> String, and printf "%d%s%…