Hacker News Reader

I 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.

Pardon 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)?

No, 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.

Refinement 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.