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

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/672efcd784528b7d0b7e17ad9c115292 https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c...