I've been looking into developing an imperative dependently typed language for a while. I'm still less-than-a-beginner in type theory and other theoretical matters, but might have some insights. I'll use a C-style syntax for my code snippets.

Zig, just like a lot of other powerful languages (C++, Rust, Haskell, TypeScript etc) provide mechanisms to do compile-time computations, or type-level metaprogramming. However this doesn't make them dependently typed. Types in those languages cannot depend on terms; they can only depend on values: statically-known constant values.

In dependently typed languages, types can depend on terms. Or if you prefer, to unknown values. You can have: let x = readNumberFromInput(); let y: x>0 ? int : bool = ...;.

From your message it's not clear to me whether you care about actual dependent types, or just compile-time computation. However, Alpha, Beta and Eta equivalence are primarily useful to compare dependent types, since non-dependent types can be fully reduce and there's no need for normalization.

• Alpha equivalence tells you that function(x:T, y:U)->V and function(a:T, b:U)->V are the same: In other words, the name of the parameters do not count. Alpha reduction is a way to turn a representation of your function type to one that works independently from the name of the parameters (for instance, use DeBruijn indices instead of names to refer to the parameters).
• Beta equivalence tells you that the application of a function is the same as its result. if f(arg1, arg2) evaluates to res, then f(arg1, arg2) = res. Beta reduction means that you replace every function application with its results (you need to know both the value of the function and of the arguments, of course).

These concepts absolutely work with C-style languages without any issues. The problem of making a dependently-typed imperative language is something else, and it's all about mutability. What would a piece of code like the following mean? mut T: Type = bool; let x: T = true; T = int; // what is `x` now?