For those who are wondering whether types can be computed in the same way as values -- yes, they can, with a proper type system. Idris [1] is a prominent exampl

For those who are wondering whether types can be computed in the same way as values -- yes, they can, with a proper type system. Idris [1] is a prominent example of a programming language with first-class types, meaning that if you can perform (finite) computation on values, you can do so on types. The difference between Idris and TypeScript (Rust, C++, etc.) is that the former treats types as values, and therefore has no traditional separation of values and types; everything is done with the same syntax. Zig strives to use the same syntax for metacomputation, although its approach is not tightly integrated into the type system, which is why you'd see compilation errors at expansion, not function definition. [1] https://www.idris-lang.org/ https://www.idris-lang.org/