Nix-effects: a dependent type checker in pure Nix

Development
1

A couple days ago I posted about using builtins.genericClosure as a trampoline. The trampoline was never the point. It was the thing that made another project tractable.

nix-effects is a Martin-Löf Type Theory proof checker embedded in pure Nix. About 3,000 lines, no evaluator patches, no external tools. Dependent functions, dependent pairs, identity types with J, cumulative universes. It runs at nix eval time, using the same core algorithms as Mini-TT and the elaboration-zoo: NbE, bidirectional type checking, de Bruijn indices.

git clone https://github.com/kleisli-io/nix-effects

I realize “dependent types in Nix” sounds like a stunt. It’s sound because of Pedrot & Tabareau’s Fire Triangle (POPL 2020): dependent types work in any language without observable effects, and Nix evaluation is pure. It’s feasible because of the trampoline. Neither is sufficient on its own.

What you can prove

Arithmetic, list operations, anything that computes to a normal form:

H = fx.types.hoas;
inherit (H) nat eq checkHoas natLit refl;

# 3 + 5 = 8. The kernel normalizes both sides and checks they agree.
checkHoas (eq nat (add (natLit 3) (natLit 5)) (natLit 8)) refl

The equality-proofs.nix file implements congruence, symmetry, transitivity, and transport via the J eliminator, all type-checked with abstract variables, so they hold universally.

From proofs to Nix functions

A proof checker that only checks proofs is a curiosity. The part I actually care about is v.verify: write a term, type-check it against a spec, and extract a plain Nix function. The proof disappears and what you get back is an ordinary Nix value.

# Verified addition: type-checked, then extracted as a Nix function
addFn = v.verify (H.forall "m" H.nat (_: H.forall "n" H.nat (_: H.nat)))
                 (v.fn "m" H.nat (m: v.fn "n" H.nat (n:
                   v.match H.nat m {
                     zero = n;
                     succ = _k: ih: H.succ ih;
                   })));

addFn 2 3  # -> 5, plain Nix integer

There’s a combinator library (v.fn, v.match, v.if_, v.map, v.filter, v.fold, v.field, v.strEq, v.strElem) so you don’t have to write raw kernel terms. verified-functions.nix has 16 examples from successor through composed filter-then-fold pipelines.

Proof-gated derivations

This is a contrived example, but it should be enough to show the shape of what I’m working toward. typed-derivation.nix defines a service config as a kernel record type and a policy function the kernel evaluates at type-checking time. The builder demands Refl : Eq(Bool, policy(cfg), true) before it constructs a derivation. If the proof fails, nix eval aborts. Nothing is built.

# Builds: localhost HTTP on 8080 passes all policy checks
api-server = mkVerifiedService {
  name = "api-server"; bind = "127.0.0.1";
  port = "8080"; protocol = "http"; logLevel = "info";
};

# Eval aborts: 0.0.0.0 with HTTP violates the cross-field invariant
insecure-public = mkVerifiedService {
  name = "insecure-public"; bind = "0.0.0.0";
  port = "80"; protocol = "http"; logLevel = "debug";
};

The policy validates each field against an allowed set and enforces that public binds require HTTPS. A separate verified function forces the effective protocol to HTTPS for public binds by construction. The invalid config never produces a derivation because the kernel normalizes policy(cfg) to false and the proof obligation Refl : Eq(Bool, false, true) gets rejected.

To be absolutely clear: this example is ad-hoc. You could do the same validation with a few assert statements.

Try it:

nix build --impure --expr '
  let pkgs = import <nixpkgs> {};
      fx = import ./nix-effects { inherit (pkgs) lib; };
  in (import ./nix-effects/examples/typed-derivation.nix { inherit fx pkgs; }).api-server'
./result/bin/api-server

What it doesn’t do

It’s fuel-bounded (default 10M steps), so it’s a partial proof checker, not a theorem prover. No user-defined inductive types. No IDE support; errors come from nix eval with blame context, which is workable for small proofs and painful for anything bigger. Nix is untyped, so the HOAS encoding can’t enforce parametricity the way PHOAS does in Coq. Exotic terms fail at type-checking time rather than being ruled out by the host.

For context: Dhall, Nickel, and CUE all require leaving Nix. The NixOS module system can express value-dependent option types (via config references), but doesn’t lend itself to formally reasoning about whether modules compose soundly. nix-effects stays inside pure Nix with the longer-term aim of kernel-checked composition, which is the tradeoff I wanted.

Links

If you’re interested in the proof theory, I’d appreciate eyes on the kernel. The implementation is in types/kernel.nix (NbE, bidirectional checking, universes) and types/hoas.nix (elaboration from HOAS to de Bruijn), and there’s a kernel spec that documents the typing rules and evaluation semantics. I want people to find errors. A soundness bug in the kernel means the whole verification story is wrong, and I’d rather know now than after someone builds on it.

The thing I keep going back and forth on is whether the right use case is proof-gated derivations (like the service config example), or something more like dependent module types for NixOS options where the type of one option depends on the value of another. Has anyone run into configuration invariants that assert or mkOption types can’t express?

14 Likes
2

Amazing work, but

is not true:

{ config, lib, … }:
let
  inherit (lib) mkOption types;
in
{
  options = {
    a = mkOption {
      type = types.bool;
    };
    b = mkOption {
      type = if config.a then types.int else types.str;
    };
  };
}

The module system is sufficiently dependently typed to do rather fancy things. It doesn’t lend itself to proper proof checking, but that’s still more powerful than most stuff out there.

4 Likes
3

You’re right, that line was sloppy and I’ve edited the post to fix it.

The module system can absolutely express value-dependent option types via config references. What I should have said is that it doesn’t lend itself nicely to formal reasoning about module composition, which you already noted. Two modules can each be internally consistent but break invariants when they merge. Today you catch that as a type mismatch error. The direction I’m interested in is whether you can state composition invariants as proof obligations in the kernel, so the failure is a rejected proof rather than a confusing eval error, and build those dependent module types from HOAS combinators so they compose by construction.

None of that is built yet, so the claim I made was both wrong on its face and a bad stand-in for the actual point. I’ve updated the post to say what I actually meant. Thanks for the correction.

2 Likes