4 ms·
> Dependent types are types that depend on values. Like this? fn f(comptime x: bool) if (x) u32 else bool { return if (x) 0 else false; }
by matklad 1y ago
> Dependent types are types that depend on values.
Like this?
fn f(comptime x: bool) if (x) u32 else bool {
return if (x) 0 else false;
}
- edflsafoiewq 1y agoNo, dependent types depend on runtime values.
- matklad 1y agoYeah, that one Zig can not do, hence "-lite".
- pcwalton 1y agoThe point is that comptime isn't dependent types at all. If your types can't depend on runtime values, they aren't dependent types. It's something more like kind polymorphism in GHC (except more dynamically typed), something which GHC explicitly calls out as not dependent types. (Also it's 12 years old [1]). [1]: https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf
- pcwalton 1y agoThat's still just a function of type ∀K∀L.K → L with a bound on K. From a type theory perspective, a comptime argument, when the function is used in such a way as to return a type, is not a value, even though it looks like one. Rather, true or false in this context is a type. (Yes, really. This is a good example of why Zig reusing the keyword "comptime" obscures the semantics.) If comptime true or comptime false were actually values, then you could put runtime values in there too.