An Experiment in Heterogeneous Software Builds
An experiment report on metaBuilder, a typed builder DSL we built to test whether ornaments are what relate heterogeneous build descriptions, and what held under test once we did.
kleisli blog
Applying effect systems and type theory to infrastructure.
Latest posts
Dependent Types in Pure Nix
nix-effects embeds a Martin-Löf Type Theory proof checker in pure Nix. Dependent functions, dependent pairs, identity types with J, cumulative universes, verified extraction of plain Nix functions from proof terms. The whole system runs at nix eval time.
Trampolining Nix with genericClosure
Nix has no loops and no tail-call optimization. builtins.genericClosure, the package dependency primitive, doubles as a general-purpose trampoline once you break the thunk chain.
Agent Coordination Is a Distributed Systems Problem
AI agent sessions are distributed processes: private state, independent failure, concurrent access to shared resources. Event sourcing gives sessions durable history; CRDTs give them convergent merge, with correctness guarantees that are purely algebraic, requiring no network model.