Proof that type systems are nothing else that domain-specific languages that run at compile time. When seen like that, it should be no surprise that they can be coerced to do general computation.
Eventually we need to make type systems just metaprogramming using the primary language that they're intended for. There's no reason for those to be two languages.
The issue with meta programming is that it’s too powerful, in the sense that the transformations can’t be statically checked for typing rules.
It doesn't matter how flexible the macro programming is, if it reduces statically to something you can typecheck, therefore this artificial segregation of syntax and rules (and mental models) represents us solving a problem superficially, in an almost cargo-cult way, because we never stopped long enough to think about at depth.
I think the issue is that the vast minority of logic is statically checkable, so your type-level logic would have so many weird restrictions that you couldn't use the full syntax anyway. So it's actually beneficial to keep them separate.
Nim is like this and its fantastic. None of the weird special rules for metaprogramming, just Nim code manipulating ASTs at compile time procedurally. Can even use standard library.
I'd love to know if anyone could reproduce the N-queens example in Nim: https://www.richard-towers.com/2023/03/11/typescripting-the-...
I believe it is possible, but don't have the time to try it out.
> The Nim compiler includes a simple linear equation solver, allowing it to infer static params in some situations where integer arithmetic is involved.
From: https://nim-lang.org/docs/manual_experimental.html#concepts-...
Probably stupid question, but that probably means that one could, theoretically, implement a type system for any one of those DSL(-like) type systems, isn't that correct? And so on and so forth, we could have, theoretically, DSL-like type systems all the way down.
The most generic one I know of is Idris. It uses some heuristics to make some functions decidable that in theory should not be.
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.
(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.)
Most of them can be coerced to do general computation, especially if they have things like if-branch, and some sort of self-reference.
But this is only true for certain languages. Overall most type systems are not Turing complete and therefore not suited for general computation