@pithlessly · github · λ

The comptime calculus

Date: 2025-06-03

This is an attempt at formalizing some aspects of Zig’s comptime. We have three types of binders:

• Ordinary lambda binders ($\lambda$) can capture variables and be applied arbitrarily, but are not dependent. They correspond to a function like fn f(x: A) B {}.
• Static lambda binders ($\lambda_s$) cannot capture variables. They correspond to a function like fn f(comptime x: A) B {}, where x is not free in B. Their argument must be provided at compile time, and type checking the body is deferred until they are called.
• Generic lambda binders ($\Lambda_s$) cannot capture variables. They correspond to a function like fn f(comptime x: A) B(x) {}. Their argument must be provided at compile time, and the type checking of both the body and the return type is deferred until they are called.

Conventions:

• Uppercase Latin letters range over terms.
• Lowercase Latin letters range over values (a subset of terms).
• Except $x$, which ranges over variables.
• $\Gamma$ ranges over contexts (which map names to types).
• $*$ is a particular value.
• All types of lambda binders are expressions. Binders are annotated with their argument and return types, which we sometimes omit for brevity.

We will be simultaneously defining two relations:

We only evaluate closed terms.

Note the general trend: as we move from $\lambda$ to $\lambda_s$ to $\Lambda_s$, we gradually move more of the premises from $\text{Ty-Foo}$ to $\text{Ty-App-Foo}$.