3 ms·
Taken literally the claim isn’t true - a Turing complete type system can enforce any constraint that a Turing complete programming language can. But your everyd
by jahewson 5y ago
Taken literally the claim isn’t true - a Turing complete type system can enforce any constraint that a Turing complete programming language can. But your everyday type systems typically can’t express concepts like “a list of at least 3 elements” or “a number which is a power of 2”.
- SCLeo 5y agoPardon my ignorance, but can this spec thing automatically deduce that 8^n evaluates to "a number which is a power of 2" or log(2, "a number which is a power of 2") is an integer? If yes, then I agree this is super helpful (and magical). If not, how is this different from a normal constrcutor (with runtime input validation)?
- travisjungroth 5y agoNo, it's not automatic like that. You define predicate functions that need to evaluate to true to pass. One of the reasons this is better than a normal constructor is these predicate functions are attached outside of the function they're describing. So they're inspectable and composable.
- jwhitlark 5y agoI think he's referring to the fact that you have more information at runtime (the actual request) than you do at compile time. But your distinction about the theoretical limitations vs the practical capabilities of current type systems is also a good point.
- mbrodersen 5y agoRefinement types and Dependent types can do all of that. But you are right that mainstream languages ca’t do that today. Hopefully that will change.