I saw that. But I don't think it has bearing on zig comptime.

zig generates a compile error when you try to pass a non-conforming type to a generic function that places conditions/restrictions on that type (such as by calling a certain predicate on instances of that type).

It's probably important to note that parametricity is a property of specific solution spaces, and not really in the ultimate problem domain (writing correct and reliable software for specific contexts), so isn't necessarily meaningful here.

> zig generates a compile error when you try to pass a non-conforming type to a generic function that places conditions/restrictions on that type (such as by calling a certain predicate on instances of that type).

Sure, but only after it's fully expanded, which is much harder to debug. And if a generic function doesn't fail to compile but rather silently behaves differently (e.g. if it calls a function that behaves unexpectedly, but still exists, on the type in question) then you don't get an error at all.

> parametricity is a property of specific solution spaces, and not really in the ultimate problem domain (writing correct and reliable software for specific contexts)

Nonsense. Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems.

> Sure, but only after it's fully expanded,

Code goes into the compiler. Either compiled code or errors come out. There's no partial expansion step to cause confusion.

You're probably referring to something about the flexibility zig's comptime allows, but it's important to note a zig programmer can be as picky as they want about what types a generic function will accept. People are really just talking about what the syntax for expression type restrictions is.

> Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems.

You can hold that opinion, but it's not a fact. The overall question isn't binary. It's one of balancing complexity and flexibility. A fixed system for specifying type restrictions is simpler and provides fewer opportunities for mistakes (assuming it's well designed), and may have parametricity. However, the lack of flexibility can just push the complexity elsewhere, e.g., leading to convoluted usage patterns, which could lead to more mistakes. A programmable system for specifying type restrictions offers more flexibility at the cost of more up-front complexity, but in a well-designed system the flexibility could lead to less overall complexity, and fewer mistakes. A nice thing about zig's approach is that the generics metaprogramming language is pretty much the same as the regular language, which mitigates the increase in complexity. I actually think it should be possible to create some kind of generics system that could credibly be said to be programmable and have parametricity, though I don't think there's any point to doing so.

> Code goes into the compiler. Either compiled code or errors come out. There's no partial expansion step to cause confusion.

You could make the same argument against having a separate compilation step at all - code goes into the language, it gets executed, any other step would just add confusion. But most of us tend to find that having a compilation step that catches errors earlier is helpful and makes it easier to produce correct code. Similarly, being able to build and check generic code as-is (in the simplest case, because generic code really is just parametric code and isn't getting monomorphised) is a lot nicer than only being able to build and check individual expansions of it.

> the lack of flexibility can just push the complexity elsewhere, e.g., leading to convoluted usage patterns, which could lead to more mistakes. A programmable system for specifying type restrictions offers more flexibility at the cost of more up-front complexity, but in a well-designed system the flexibility could lead to less overall complexity, and fewer mistakes

Some way of doing ad-hoc polymorphism is probably desirable, but only if it's set up so that people don't default to it. Generic things should be parametric most of the time, and non-parametricity should be visible, so that people don't do it accidentally. It's similar to e.g. nullability - yes, you probably do want to have some way to represent absent/missing/error states, but if you just make every value nullable and say that any function that wants non-nullable inputs can check itself, that "flexibility" ends up being mostly ways to shoot yourself in the foot.

> Generic things should be parametric most of the time, and non-parametricity should be visible, so that people don't do it accidentally.

Economy of mechanism is powerful though, it's one of the reasons C is still so popular. The comptime approach that provides both parametric and ad-hoc polymorphism using a single mechanism seems to fit Zig quite well. I'm still a bit of a typaholic, but I've really come to appreciate economy of mechanism instead of deeply inscrutable types.

I think a good language would take something like Zig's approach to comptime, where the template/macro language is the same as the value language, with a deep consideration of TURNSTILE from "Type Systems as Macros":

https://www.khoury.northeastern.edu/home/stchang/pubs/ckg-po...

You can even get to dependent type systems as macros:

https://www.williamjbowman.com/resources/wjb2019-depmacros.p...

I think a good design would involve stage polymorphism, but it does need to be the kind of polymorphism that preserves the distinction rather than just smooshing stages together or having ad-hoc special cases. (I've gone through this in the past, with Java 1.2 style types vs untyped vs typed with polymorphism, or more recently with the "function colouring" debate; Rust-style linearity is heading in the same direction too).

As far as I can see from a quick skim your links are one meta level up, about using macros to implement a type system for a DSL (which may have polymorphism and the like within that DSL) rather than using them to implement typing itself. There's still a distinction between types and macros, it's just that macros are being used to process types.

> rather than using them to implement typing itself.

I'm not sure what this means exactly. Those papers do use macros to implement extensible/pluggable static type systems just like those we use every day. The point is that the phase distinction is respected as macros run at compile-time. If your macro language roughly matches your value language, then this would look something like Zig, but more expressive, and the compilation output is a residual program that can run without types (although runtime type embeddings are also possible where needed).

The problem I have with typing all of this is that I haven't yet found a satisfactory approach that doesn't explode into a typing zoo that's only usable for niche experts. Economy of mechanism is very important for wider adoption IMO. People can debug ordinary programs, so if your compiler runs your source program like an ordinary program, they can straightforwardly debug that too if this is designed well.

> Nonsense. Without parametricity your software is not compositional and it becomes impossible to write correct software to solve complex problems.

In theory there is no difference between theory and practice. In practice there is.