[matklad]

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.

[pcwalton]

> 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.

[1]: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/poly...

[matklad]

> 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;
    }

[pcwalton]

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.

[edflsafoiewq]

No, dependent types depend on runtime values.

[matklad]

Yeah, that one Zig can not do, hence "-lite".

[pcwalton]

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]).

[1]: https://www.seas.upenn.edu/~sweirich/papers/fckinds.pdf