@pithlessly · github · λ

The comptime calculus

Date: 2025-06-03
Last updated: 2025-11-06

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.
• Types are a particular kind of value.
• $*$ is a particular type (the type of types).
• $\Gamma$ ranges over contexts (which map names to types).
• All varieties of lambda binders are values. Binders are annotated with their argument and return types, which we sometimes omit for brevity.

We will be simultaneously defining two relations:

$$\begin{aligned} \boxed{ \Gamma \vdash M : a } & \qquad \text{ $M$ has type $a$ in $\Gamma$ } \\ \boxed{ M \leadsto z : a } & \qquad \text{ $M$ evaluates to $z$ at type $a$ } \end{aligned}$$

We only evaluate closed terms.

$$\begin{aligned} \boxed{\text{ Eval-Val }} & \qquad \frac{ \cdot \vdash z : a }{ z \leadsto z : a } \\\\ \boxed{\text{ Ty-$\lambda$ }} & \qquad \frac{ A \leadsto a : * \qquad B \leadsto b : * \qquad \Gamma, x : a \vdash E : b }{ \Gamma \vdash (\lambda (x : A) \to E : B) : a \to b } \\\\ \boxed{\text{ Ty-App-$\lambda$ }} & \qquad \frac{ \Gamma \vdash E_1 : a \to b \qquad \Gamma \vdash E_2 : a }{ \Gamma \vdash E_1(E_2) : b } \\\\ \boxed{\text{ Eval-App-$\lambda$ }} & \qquad \frac{ E_1 \leadsto (\lambda x \to E') : a \to b \qquad E_2 \leadsto v_2 : a \qquad [v_2 / x]E' \leadsto v' : b }{ E_1(E_2) \leadsto v' : b } \\\\ \boxed{\text{ Ty-$\lambda_s$ }} & \qquad \frac{ A \leadsto a : * \qquad B \leadsto b : * }{ \cdot \vdash (\lambda_s (x : A) \to E : B) : a \to_s b } \\\\ \boxed{\text{ Ty-App-$\lambda_s$ }} & \qquad \frac{ E_1 \leadsto (\lambda_s x \to E') : a \to_s b \qquad E_2 \leadsto v_2 : a \qquad \cdot \vdash [v_2/x] E' : b }{ \cdot \vdash E_1(E_2) : b } \\\\ \boxed{\text{ Eval-App-$\lambda_s$ }} & \qquad \frac{ E_1 \leadsto (\lambda_s x \to E') : a \to_s b \qquad E_2 \leadsto v_2 : a \qquad [v_2/x] E' \leadsto v' : b }{ E_1(E_2) \leadsto v' : b } \\\\ \boxed{\text{ Ty-$\Lambda_s$ }} & \qquad \frac{ A \leadsto a : * }{ \Gamma \vdash (\Lambda_s (x : A) \to E : B) : \forall (x : a) \to_s B } \\\\ \boxed{\text{ Ty-App-$\Lambda_s$ }} & \qquad \frac{ E_1 \leadsto (\Lambda_s x \to E') : \forall (x : a) \to_s B \qquad E_2 \leadsto v_2 : a \qquad [v_2/x] B \leadsto b : * \qquad \cdot \vdash [v_2/x] E' : b }{ \cdot \vdash E_1(E_2) : b } \\\\ \boxed{\text{ Eval-App-$\Lambda_s$ }} & \qquad \frac{ E_1 \leadsto (\Lambda_s x \to E') : \forall (x : a) \to_s B \qquad E_2 \leadsto v_2 : a \qquad [v_2/x] E' \leadsto v' : b }{ E_1(E_2) \leadsto v' : b } \end{aligned}$$

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}$.