"Algebraic" effects in Zig

We feel like we haven’t explained this claim we made that Zig supports algebraic effects.

In Lean, let’s say we have two monad A : x -> Type and B : x -> Type.

We then must have this:

def Pair (A B : Type → Type) (x : Type) : Type := A x × B x

instance [Monad A] [Monad B] : Monad (Pair A B) where
  pure a := (pure a, pure a)
  bind p f := (p.1 >>= fun a => (f a).1, p.2 >>= fun b => (f b).2)

-- an "allocator" that counts bytes, and a random source
abbrev AllocM := StateM Nat
abbrev RandM := StateM StdGen

def allocSide (n : Nat) : AllocM ByteArray := do
  modify (· + n)
  return ByteArray.mk (Array.replicate n 0)

def randSide (n : Nat) : RandM ByteArray := do
  let mut out := ByteArray.empty
  for _ in [0:n] do
    let (b, g') := randNat (← get) 0 255
    set g'
    out := out.push b.toUInt8
  return out

def randomBytes (n : Nat) : Pair AllocM RandM ByteArray :=
  (allocSide n, randSide n)

#eval
  let (allocRun, randRun) := randomBytes 4
  let (zeroed, bytesUsed) := allocRun.run 0
  let (random, _) := randRun.run (mkStdGen 42)
  (zeroed.data.toList, bytesUsed, random.data.toList)
-- ([0, 0, 0, 0], 4, [37, 165, 219, 80])

Here’s how it’s like in Zig:

const std = @import("std");
const Allocator = std.mem.Allocator;
const Random = std.Random;

fn randomBytes(ctx: struct { a: Allocator, r: Random }, n: usize) ![]u8 {
    const buf = try ctx.a.alloc(u8, n);
    ctx.r.bytes(buf);
    return buf;
}

pub fn main() !void {
    var da: std.heap.DebugAllocator(.{}) = .init;
    defer _ = da.deinit();
    var prng: std.Random.DefaultPrng = .init(42);
    const a = da.allocator();
    const buf = try randomBytes(.{ .a = a, .r = prng.random() }, 16);
    defer a.free(buf);
    std.debug.print("{x}\n", .{buf});
}

No special Pair type needed.

Kimi K3’s stance:

The claim is right in spirit and wrong in the letter, and the real examples above show where. In Lean, randomBytes is a value living inside the product of two computations; look at the output: one run returns a zeroed buffer and a byte count, the other returns random bytes. The two sides never meet — nothing ever fills the allocated buffer. In Zig, randomBytes is a function consuming the product of two handlers, and ctx.r.bytes(buf) fills the very buffer ctx.a.alloc returned. Same name, opposite roles.

This is structural, not incidental. Pair A B keeps the two monads sealed apart: bind threads each component separately, so no single Pair-computation can use both A and B. Meanwhile the Zig function uses ctx.a and ctx.r in the same body, and the “bind” is the semicolon. One function using two effects together is exactly what the product of monads cannot express, and what the product of handlers does trivially. The theorem that describes the Zig side is currying: randomBytes is a computation in Reader (Allocator × Random), and Reader (A × R) T ≅ A → R → T. The Pair instance remains a true theorem that the Zig code never uses.

Which is to say: Zig’s answer to algebraic effects is to not have them. An Allocator is a handler — a ptr plus a vtable, an interpreter passed by hand. anytype makes foo polymorphic over handlers. The effect system is the calling convention.

What you give up: resumable continuations (a Zig handler returns a value; it cannot suspend the caller and resume later) and effect tracking (nothing stops randomBytes from allocating through a global instead of ctx.a; the discipline is social, not static). Real effect languages buy those two with a lot of machinery. Zig declines the machinery, and the purchase.

I approve of the practice. But the proof obligation runs the other way: the correct formalization is the Reader stack, and the honest name is effects as parameters.