Commiting Dependent Type Crimes in Zig

If you thing Zig is just another C-level language, you haven’t typed enough. Zig’s struct-in-a-fn feature allows dependent types with ergonomic syntax.

Recently, I was doing a large software project. I started the project in Rust, but switched to Zig because Rust is too limiting.

The API I’m targeting is very uniform. Its routes all look like this:

• HTTP POST
• static URL
• input as POST payload (shape described in schema)
• output as response body (shape described in schema)

Here’s what I came up with.

/// API route
pub const Route = struct {
    /// endpoint url like /i
    url: []const u8,
    /// uplink type (request body)
    Tup: type,
    /// downlink type (response body)
    Tdown: type,

    pub fn init(comptime url: []const u8, comptime Tup: type, comptime Tdown: type) @This() {
        return .{ .Tup = Tup, .Tdown = Tdown, .url = url };
    }
};

In Rust, this would have to be like Route<Tup, Tdown>. Jankier solutions exist, but I’d rather write simple code.

Then, I described some routes plus input and output types.

pub const routes = struct {
    pub const whoami = Route.init("i", struct {}, types.UserLite);
    ...
};

pub const types = struct {
    pub const UserLite = struct {
        id: []const u8,
        name: []const u8,
        username: []const u8,
    };
};

With the API definition done, I moved onto the HTTP client. It came out looking like this.

/// Request manager with retry. Manages a client, a thread, and a single API route.
pub fn Resource(comptime route: Firefish.Route) type {
    return struct {
        ...
    };
}

Dear reader, if you still think that this looks perfectly normal, I have to remind you that putting type in term is only possible in Idris, Lean, or Zig. Zig is not like the other two, since its type system is much simpler. It somehow retains the ability to mix term and type freely, which neither D nor Nim can.

Even if I invented a programming language already, I don’t think I can think up Zig’s syntax for “generics” in my lifetime. Hail Andrew Kelley and Josh Wolfe! ¹

One thing Zig’s type system pains me is the verbosity of “inline functions”. To include function inside function, you currently have to do

fn foo() void {
    const o = struct {
        fn bar() void {}
    };
    const bar = o.bar;
}

There are attempts to resolve this issue. However, async/await will have to come first. It seems like this feature is not going to be added to Zig, in the name of encouraging explicit control flow.

Also, by the time you are reading this, Zig 0.11 (stable release) is probably out. Now go try it!

P.S. You can also pass functions around in Zig just like in C, but more type checked. A function and a pointer to a function are two different concepts in Zig.

Edit: My site has been lobstered for the first time! I think my writing is too simple, and the concept of putting types in terms may be hard to understand. For more information, please re-read.

Edit: Here are some more example code.

The Idris Door Example

pub fn main() !void {
    const d0 = Door(.closed){};
    const d1 = d0.open();
    const d2 = d1.open(); // type error
    _ = d2;
}

const DoorState = enum { open, closed };

fn Door(comptime state: DoorState) type {
    return switch (state) {
        .open => struct {
            fn close(_: @This()) Door(.closed) {
                return .{};
            }
        },
        .closed => struct {
            fn open(_: @This()) Door(.open) {
                return .{};
            }
        },
    };
}

Type-level Integer

pub fn main() !void {
    const c0 = Counter(0){};
    const c1 = c0.inc();
    const c2 = c1.inc();
    _ = c2;
    // @TypeOf(c2) == Counter(2)
}

fn Counter(comptime i: comptime_int) type {
    return struct {
        fn inc(_: @This()) Counter(i + 1) {
            return .{};
        }
    };
}

Footnotes