Comment by andyferris

Zig's sub-language and evaluation rules are exactly the same as the Zig language except that `type` is a first class type and the TypeInfo of any type can be both examined and modified. In Zig, generics are implemented by computing types--most often by a function returning a struct that is specialized to a type argument to the function.

I've been writing some D code and, while D "template" functions can take compile-time arguments that are types, they can only produce types via mixins, which are strings that are injected at the point of invocation and then parsed by the compiler. This gives you all of the power of Zig and then some, but it's not nearly as elegant (it would help a lot if D's token quote construct q{...} had lisp-like quasi-quote functionality). OTOH, I found when writing Zig it could become extremely confusing to have the comptime and runtime languages intermixed, which is often done for loop unrolling and "conditional compilation" -- whether it's a comptime or runtime operation is in many cases a function of whether the variables involved are comptime or runtime types. In D it's generally clearer because comptime operations are distinguished with such things as static if for flow control, enum for declaring comptime variables, foo!(comptime args)(runtime args) for function calls, etc.

Sorry if this is obvious, but do these languages let programmers explicitly assert that a certain, relevant property holds at runtime?

Or do these compilers insist on working these proofs out on there own without the benefit of programmer-supplied assertions?

If you don’t know at compile time what the type of the value is that is returned, how do you know whether the remainder of the expression is still correct?

The choice is either to have a total function that will be able to deal with every type and check at compile time whether they exist or to defer to the runtime and then throw an exception if the program doesn’t know what to do with the value.

I commented this before but deleted it because I hadn't tested my code properly. Anyway, here is a version that works.

You're right Zig isn't quite as powerful, but you don't need type erasure if you have enough monomorphization. It's a bit annoying to use since you have to capture the comptime version of b inside the inline switch prongs, and get_value does need to take a comptime bool instead of a runtime one. It's functionally the same, except that instead of using the bool to prove the type of the type-erased value is correct and delaying the actual if (b) check to runtime, we're moving it to compile time and instead proving that b has the right value for each case, then generating specialized code.

This does NOT mean that it isn't dependent on user input, the call do_thing(get_user_input()) would absolutely work. do_thing has no compile-time parameters at all.

I don't have the natToString thing because it's a bit more annoying in Zig and would obscure the point.

    const std = @import("std");
    
    fn get_value(comptime b: bool) if (b) u32 else []const u8 {
        if (b) return 12
        else return "string";
    }
    
    fn do_thing(b: bool) void {
        switch (b) {
            inline true => |known_b| std.log.info("{d}", .{get_value(known_b)}),
            inline false => |known_b| std.log.info("{s}", .{get_value(known_b)}),
        }
    }
    
    pub fn main() void {
        do_thing(true);
        do_thing(false);
    }

    fn pick_type(comptime b: bool) type {
        if (b) return u32 else return []const u8;
    }

    fn get_value(comptime b: bool) pick_type(b)

Perhaps more convincingly, you can use inline for with a similar effect. It's obviously horrible code nobody would ever write but I think it might illustrate the point.

    fn do_thing(b: bool) void {
        inline for (0..2) |i| { // go through all bool variants
            const known_b = (i != 0);
            
            if (known_b == b) {
                // Essentially what we have now is a known_b which is proven
                // at compile-time to be equal to whatever runtime b we have.
                // So we're free to do any kind of dependent type things we'd like
                // with this value.
                
                const value = get_value(known_b);
                // Here we know the type of value but it still depends on the runtime b.
                
                if (known_b) std.log.info("{d}", .{value}) // treated as an int
                else std.log.info("{s}", .{value}); // treated as a string
                
                // We can also just decide based on the type of value at this point.
                if (@TypeOf(value) == u32) ... else ...;
                // Or, a switch
                switch (@TypeOf(value)) {
                    u32 => ...,
                    []const u8 => ...,
                }
            }
        }
    }