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...
[1]: https://gist.github.com/chrisdone/672efcd784528b7d0b7e17ad9c...
No comments yet.