> else that domain-specific languages that run at compile time.
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 difference between regular languages and "type system languages" (at least well designed ones) is that the latter are decidable. In that sense another typesystem lang for the typesystem lang would still be a decidable one.
The most generic one I know of is Idris. It uses some heuristics to make some functions decidable that in theory should not be.
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.