It is weird to me that so many people are getting caught up on the fact that type safe printf has been around forever. If someone has looked into Idris they almost certainly know that it isn't a new concept.

I linked it because its implementation is amazing comparatively and it is just one clean example of what is possible.

It's been almost a decade since I used Apache Groovy, but I don't remember its printf being type safe. Its method signature is

  void Object.printf(String, Object)

and it evaluates types at runtime.

I used it in OCaml well before there was a Groovy. But what's interesting here is that you get it without compiler special casing and without macros, as a natural consequence of how the type system works - in a way that generalizes to other problems.

>without macros

Type systems are macro systems, it's just not obvious because type languages are very different from expression languages. The main "innovation" of Idris is hammering harder on this front. And in any case, the fact that most type languages are logic languages gives people with a formalist bent a warm feeling in their stomachs.

There's a valid perspective from which type systems are particularly-constrained macro systems. That doesn't mean there aren't contexts where it's useful and/or interesting to distinguish. But if you wish, pretend I had written "traditionally conceived general purpose macros" :)

I know clang will not let you make a mistake, but it must be some kluge since the C language clearly doesn't anticipate that.