>for Zig enthusiasts, the set of features that Zig has appeals to them. Just like enthusiasts of every programming language.
I find it rather amusing that it's a Java and a Rust enthusiast who are extolling Zig approach here! I am not particularly well read with respect to programming languages, but I don't recall many languages which define generic pair as
fn Pair(A: type, B: type) type {
return struct { fst: A, snd: B };
}
The only one that comes to mind is 1ML, and I'd argue that it is also revolutionary.
Well, if you strip away the curly braces and return statement, that's just a regular type definition. Modeling generic types as functions from types to types is just System F, which goes back to 1975. Turing-complete type-level programming is common in tons of languages, from TypeScript to Scala to Haskell.
I think the innovation here is imperative type-level programming--languages that support type-level programming are typically functional languages, or functional languages at the type level. Certainly interesting, but not revolutionary IMO.
The thing is, this is not type-level programming, this is term-level programming. That there's no separate language of types is the feature. Functional/imperative is orthogonal. You can imagine functional Zig which writes
Pair :: type -> type -> type
let Pair a b = product a b
This is one half of the innovation, dependent-types lite.
The second half is how every other major feature is expressed _directly_ via comptime/partial evaluation, not even syntax sugar is necessary. Generic, macros, and conditional compilation are the three big ones.
> This is one half of the innovation, dependent-types lite.
But that's not dependent types. Dependent types are types that depend on values. If all the arguments to a function are either types or values, then you don't have dependent types: you have kind polymorphism, as implemented for example in GHC extensions [1].
> The second half is how every other major feature is expressed _directly_ via comptime/partial evaluation, not even syntax sugar is necessary. Generic, macros, and conditional compilation are the three big ones.
I'd argue that not having syntactic sugar is pretty minor, but reasonable people can differ I suppose.
That'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.
The 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]).
I find it rather amusing that it's a Java and a Rust enthusiast who are extolling Zig approach here! I am not particularly well read with respect to programming languages, but I don't recall many languages which define generic pair as
The only one that comes to mind is 1ML, and I'd argue that it is also revolutionary.