Comment by ChadNauseam

Comment by ChadNauseam 11 hours ago

I'm not familiar with Zig, but I'm pretty sure comptime is not quite as powerful.

In the post, I didn't give any examples of situations where the input to a dependent function was not known at compile time. However, that was just due to the lack of time when writing the post.

I gave this example:

    useValue : Bool -> String
    useValue True = "The number is: " ++ natToString (getValue True)
    useValue False = "The message is: " ++ getValue False

The difference is that nothing in dependent types requires that the depended-on value `b` is known at compile time. You could pass any Bool to `getValue`, including one that was read as input from the user. It would just be the case that, before using the value returned by `getValue b`, you'd have to check (at runtime) the value of `b`. Only then would you know `pickType b`, which would tell you the type of `getValue b`. My apologies that the post was unclear about this. (I've just updated it.)

[removed] 6 hours ago

[deleted]

Reply View 0 replies

spockz 11 hours ago

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.

Reply View 3 replies

ChadNauseam 10 hours ago

The value returned by `getValue b` has type `pickType b`. It cannot be used in a way that depends on its type until you check the value of `b`. If `b = True`, then you know that `pickType b = pickType True = Nat` and that therefore `getValue b` has type `Nat`. There is no option to check the type of a value at runtime. You simply cannot use it in such a way as to create a runtime type error. (This is what it means for the types to be erased. The runtime doesn't know what type it's supposed to be!)

Reply View | 0 replies
rtpg 6 hours ago
getValue : (b : Bool) -> pickType b getValue True = 42 getValue False = "hello"
So given something like this, imagine something like the following:
someBool = flipACoinToGetABool thingy = getValue someBool
You're already in trouble here right? what's the type of thingy?
So maybe you write:
thingy: (pickType someBool) = getValue someBool
which is fine and great!
then you write:
print (thingy + 3) -- thingy can be an int right?
But at this point thingy is of type "pickType someBool" while + is expecting Int. So it's up to you to restructure your code to prove to the type checker that someBool is in fact True.
For example:
print ((if someBool then thingy else 5) + 3)
^ and here your code proves the fact! So in practice when you want to explore the results that are hidden behind the dependent types, you will need to have written code that unwraps it like this. But the whole point is the underpinning type theory means that you will be fine while doing it! You've proven that it'll be fine, so if you add thingy to 3 you'll have an integer.
I think of this stuff a bit like encryption password. You have this bundle of data, but to get in, you need to provide proof that what you're doing won't blow up. You'll need to write your code in a certain way to do it. But if you provide the right proof, then we're golden.
Reply View | 0 replies
skybrian 8 hours ago

Consider how Rust monomorphizes generic functions, making a copy for each possibility. I imagine a compiler could generate a different continuation for each possible return type, along with a runtime check that branches to the appropriate continuation.
It seems like that might cause code bloat, though?

Reply View | 0 replies

ioanaci 6 hours ago

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

You could define a function

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

and change the signature

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

if you wish.

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 => ...,
                }
            }
        }
    }

Reply View 0 replies