· 5 min read ·

Zig's Comptime and the Free Theorems It Breaks

Source: lobsters

Parametric Polymorphism and What It Promises

There’s a concept in type theory called parametricity, and understanding it changes how you read generic function signatures. Noel Welsh’s recent piece on comptime uses it as a lens to examine Zig, and the result illuminates something important about what it means for a type to be a contract.

Parametricity was formalized by John Reynolds in his 1983 paper “Types, Abstraction and Parametric Polymorphism”. The core idea: when a function is polymorphic over a type, it must behave uniformly across all instantiations of that type. The function has no mechanism to inspect which type it received. Philip Wadler extended this into a practical tool in “Theorems for Free!” (1989), showing that a function’s type signature alone is sufficient to derive theorems about its behavior.

Consider Haskell. A function typed id :: a -> a must be the identity function. There is no other valid implementation, because the function cannot create a value of type a from nothing, and cannot inspect what a is at runtime. The signature is a behavioral proof.

-- The only possible implementation of this type
id :: a -> a
id x = x

This is the theorem for free: without reading the source, you know that id x == x for every x. A function typed sort :: Ord a => [a] -> [a] can only rearrange its input elements; it cannot manufacture new ones or discard elements based on their values. The signature alone establishes that sort produces a permutation of its input. Zig’s comptime removes this property, and the consequences are worth examining carefully.

How Comptime Breaks Parametricity

In Zig, comptime parameters are evaluated at compile time. The standard way to write a generic function looks like this:

fn identity(comptime T: type, value: T) T {
    return value;
}

This looks parametric. However, Zig imposes no constraint that you treat T uniformly. The following is valid Zig:

fn suspiciousIdentity(comptime T: type, value: T) T {
    if (T == u32) {
        return value + 1;
    }
    return value;
}

The function shares the same signature shape as identity but returns value + 1 when instantiated with u32. The type signature communicates nothing about whether this function behaves uniformly or branches on specific types, and parametric reasoning no longer applies.

This is fundamentally different from how Rust approaches generics. In Rust, an unconstrained generic function cannot branch on the type without explicitly requesting runtime type information:

fn identity<T>(x: T) -> T {
    // Cannot inspect T without explicit trait bounds
    x
}

Rust generics are parametric by default. To get type-specific behavior, you define traits and add them to the signature. A function fn process<T: Display>(x: T) tells you exactly what capability it requires from T. The type-specific behavior is visible in the signature; you don’t need to read the body to understand what a function can and cannot do with its argument.

The C++ Precedent

Zig isn’t the first systems language to build generic facilities on type inspection. C++ templates have enabled non-parametric generics since their introduction, and with if constexpr the pattern is direct:

template<typename T>
T suspiciousIdentity(T x) {
    if constexpr (std::is_same_v<T, int>) {
        return x + 1;
    }
    return x;
}

The C++ ecosystem has built on this property for decades. Type traits, SFINAE, and if constexpr all depend on the ability to inspect types at compile time. Template metaprogramming exists largely because of it.

Where C++ accumulated these features piecemeal across many standard revisions, Zig designs around comptime as a first-class mechanism from the start. The Zig documentation on comptime presents it as a unified replacement for generics, macros, and conditional compilation. The trade-off is the same as in C++, but the design is consolidated rather than emergent from layers of template instantiation rules.

The Practical Cost of Non-Parametric Generics

The loss of parametricity has direct consequences for how you reason about unfamiliar code. In a parametric language, when you see f :: [a] -> [a], the space of possible behaviors is bounded. The function is some list transformation: reverse, sort, take, drop, filter. It cannot treat elements as integers and double them, because it doesn’t know they’re integers. That constraint alone makes code review faster and debugging more systematic.

Without parametricity, every generic function is potentially a special-case accumulator. You have to read the implementation. In a large codebase, this compounds: a utility function that appeared to be a uniform transformation might have an if T == SomeType branch added months ago for a specific case.

The ML and Haskell traditions value this constraint precisely because it makes types into verifiable documentation. OCaml’s module system relies on parametric polymorphism for the abstractions it provides. The free theorems from parametricity aren’t just mathematically elegant; they are the reason you can trust a function without auditing every line.

The Tradeoff Zig Makes

Zig chooses expressiveness over this property, and the choice is coherent given the language’s goals. Systems programmers regularly need to emit different code for different types, and Zig lets you write that logic in ordinary Zig code rather than reaching for preprocessor macros or external code generation tools.

The standard example is serialization. A generic serializer that handles primitive types, structs, and enums differently requires type inspection. In Zig:

fn serialize(comptime T: type, writer: anytype, value: T) !void {
    const info = @typeInfo(T);
    switch (info) {
        .Int, .Float => try writer.print("{}", .{value}),
        .Struct => |s| {
            inline for (s.fields) |field| {
                try serialize(field.type, writer, @field(value, field.name));
            }
        },
        else => @compileError("unsupported type"),
    }
}

The @typeInfo builtin returns a tagged union containing complete type metadata. inline for iterates at compile time over struct fields. The Zig standard library uses this pattern throughout, including in std.fmt. The equivalent in Haskell requires either typeclasses, which must be declared in the signature and thus remain visible, or a generics library like GHC.Generics or generics-sop. Both work, but the type-specific branching must surface in the type signature through class constraints. Zig’s version is more direct: you write the serializer as a function that inspects its argument’s type and generates code accordingly. The abstraction cost is that callers lose the reasoning guarantee.

Reading Generic Zig Code

For Zig programmers, the practical implication is that comptime type parameters carry less information than parametric type variables. The signature alone does not bound the behavior. Type-specific branches are possible in any generic function and, given how natural @typeInfo makes them, they appear regularly in real code.

A useful habit when writing generic Zig: if a function genuinely behaves uniformly across types and the variation is only in memory layout or size, make that intention visible in documentation or comments. If it branches on types, keep those branches prominent and legible rather than abstracted into helpers where they require excavation to find.

The broader point in Welsh’s analysis is that “generic” is not a single concept across languages. Parametric polymorphism, C++ template instantiation, Zig comptime, and Rust trait dispatch are different mechanisms with different reasoning properties. Knowing which you’re working with shapes how much you can infer from a signature. Zig’s comptime is honest about what it is: compile-time code execution with full knowledge of its type arguments. The type system does not pretend to constrain behavior it isn’t constraining, and that clarity has its own value.

Was this interesting?