Re:Types as axioms, or: playing god with static types
by valenterry on Saturday August 15, 2020 @11:54PM
(#24174914)
You are right and it seems you have a very good gut-feeling about these things! :)
What you describe is commonly called a "(value) dependent type system". There are languages that support this, e.g. Idris which was specifically built for that: https://www.idris-lang.org/
The compiler will parse the input string such as "some number %d and a string %s" at compile time (!) and assess whether the following arguments passed to printf satisfy the shape of the string.
What you describe is commonly called a "(value) dependent type system". There are languages that support this, e.g. Idris which was specifically built for that: https://www.idris-lang.org/
Here is an example where the printf function is built purely in Idris: https://paulosuzart.github.io/blog/2017/06/18/dependent-type...
The compiler will parse the input string such as "some number %d and a string %s" at compile time (!) and assess whether the following arguments passed to printf satisfy the shape of the string.