3 ms·
Some languages have type systems like that, either deliberately as in the case of Idris and Agda or accidentally as in C++ or Typescript. It doesn't have to be
by weinzierl 3y ago
Some languages have type systems like that, either deliberately as in the case of Idris and Agda or accidentally as in C++ or Typescript.
It doesn't have to be that way and in my opinion for general purpose languages it shouldn't. The type system should be about constraints that facilitate reasoning about your code - reasoning by machine and human.
Compile time computation should be a separate facility.
- WorldMaker 3y agoIt wasn't an accident in Typescript. Each step along the way seemed well deliberated and to facilitate reasoning about someone's code, despite the computational complexity trade-offs. (That a lot of that was to facilitate reasoning about nearly untyped JS code doing a lot of dynamic code things is, depending on which side of the deliberation you are on: 1] a sign that dynamic code has always been that complex and developers have had to do all that sort of "compile time logic" in their own heads for so long, and/or 2] a sign that Typescript's "flaws" come from trying to be too supportive of existing bad JS code.)