Hacker News Reader

Maybe Idris or Blodwen. Idris can at least define a printf function where the string must contain the right template, i.e. printf("number %i text %s", 5, "hey") compiles, but printf("number %s text %s", 5, "hey") does not, so I'm not sure it's impossible to encode string reversal in the type signature.

View on HN

You really don't need dependent types to do the printf thing, any language with GADTs or equivalent typing functionality can do it, see for instance OCaml's Printf module. Although you do need a little bit of magic from the compiler to get that exact syntax, which you can get rid of with dependent types.

Reply on news.ycombinator.com