I usually go with "you can make a dependent pair", which is two terms where the type of the second depends on the value of the first; I think you could do that in Zig with a bit of handwaving around whether the comptime expression really is the first value or not.
What Zig's doing is also, as best I understand it all, the only real path to anything like dependent types in imperative languages: make a separate sub-language for constant expressions that has its own evaluation rules that run at compile time. See also C++ constexpr, or the constants permitted in a Rust static array size parameter (practically a dependent type itself!)
A functional language's basic building block is an expression and terms are built out of composed expressions; normalisation means reducing a term as far as possible, and equality is (handwaving!) when two terms reduce to exactly the same thing. So you can do your dependent terms in the usual source language with the usual evaluation rules, and those terms are freely usable at runtime or compile time, it's all the same code.
An imperative language's basic building block is a memory peek or poke, with programs composed of sequences of peeks and pokes scheduled by control flow operators. It's much less clear what "normalisation" looks like here, so imperative languages need that separate constant-value embedded language.
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.
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 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.
getValue : (b : Bool) -> pickType b
getValue True = 42
getValue False = "hello"
someBool = flipACoinToGetABool
thingy = getValue someBool
So maybe you write:
thingy: (pickType someBool) = getValue someBool
then you write:
print (thingy + 3) -- thingy can be an int right?
For example:
print ((if someBool then thingy else 5) + 3)
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.
It seems like that might cause code bloat, though?
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 => ...,
}
}
}
}Note that a language with dependent types doesn't actually "generate" types at runtime (as Zig does at compile-time). It's really about managing proofs that certain runtime objects are instances of certain types. E.g. you could have a "prime number" type, and functions that compute integers would need to include a proof that their result is a prime number if they want to return an instance of the prime number type.
Using dependent types well can be a lot of work in practice. You basically need to write correctness proofs of arbitrary properties.
Or do these compilers insist on working these proofs out on there own without the benefit of programmer-supplied assertions?
Yes, but the programmer has to do the really, really, really hard work of proving that's the case. Otherwise, the compiler says: you haven't proved to me that it's true, so I won't let you make this assertion. Put another way: the compiler checks your proof, but it doesn't write it for you.
The only programs for which all interesting assertions have been proven in this, or a similar, way have not only been small (up to ~10KLOC), but the size of such programs relative to that of the average program has been falling for several decades.
You can assert something but then you also have to prove it. An assertion is like a type declaration: you're asserting values of this type can exist. The proof of that assertion is constructing a value of that type to show that it can be instantiated.
This is what the Curry-Howard correspondence means. The types of most languages are just very weak propositions/assertions, but dependent types let you declare arbitrarily complex assertions. Constructing values of such arbitrarily complex assertions can get very hairy.
If you take Zig, it's `comptime` parameters are kind of similar. They can be used to create functions that return types or whose output type depends on the inputs, etc. It seems to fulfil the three axioms at the start, no? The erasure stuff seems just as relavant.
Can I say that `comptime` is dependent types in imperative clothing? Or is there a missing capability making it strictly weaker?