Re:Idris: A Language for Type-Driven Development
by still_grokking on Saturday January 21, 2023 @05:29AM
(#34465401)
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.
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.