[mgradowski]

Dependent types could presumably capture this idea. They are very expressive – see [1] for a perfectly type-safe printf implementation in Idris.

[1]: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c...