3 ms·
That claim doesn't look correct. Zig is just doing "compile time reflection". That's not even remotely close to dependent types. The whole point of DT is that
by still_grokking 4y ago
That claim doesn't look correct.
Zig is just doing "compile time reflection". That's not even remotely close to dependent types.
The whole point of DT is that computed types can be used for type checking, and not only to compute values form them.
DT enable to reason about programs as mathematical proves. That's not possible in Zig, afaik.
If merely passing around values called "types" would be similar to what Idris does every language with runtime reflection and also all dynamic(!) languages would have DT. That's of course not true.