3 ms·
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")
by RedNifre 3y ago
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.
- deredede 3y agoYou 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.