Typed Validation

Typed validation is the first user-facing layer built on the effect model. A type describes the values a boundary accepts. The same type can answer a fast yes/no question or produce structured diagnostics through a handler.

The point is not only that validation exists. In nix-effects, validation is derived from the type description. Users write the shape and any domain refinements; they do not write a recursive validator for every record, list, variant, or generated datatype. That derive-style capability is hosted inside Nix itself, not delegated to an external schema engine or macro system.

This chapter uses value-level types. Later chapters show how generated datatypes carry reusable descriptions that the same checker, diagnostic tools, interpreters, and generic derivations consume.

Primitive and refined types

Primitive types wrap Nix value predicates with kernel-backed type information:

let inherit (fx.types) Int String Bool;
in {
  okInt = Int.check 3;
  okString = String.check "aspect";
  badBool = Bool.check "true";
}

Refinement types narrow an existing type with a predicate:

let
  inherit (fx.types) String refined;
  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);
in {
  ok = TargetClass.check "module";
  bad = TargetClass.check "fleet";
}

Use refinements for named boundary conditions: target classes, non-empty names, supported dialects, allowed protocol versions, and similar concrete constraints.

Structured values

Records and lists compose types into larger boundaries:

let
  inherit (fx.types) Record String ListOf refined;
  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  AspectDecl = Record {
    name = String;
    target = TargetClass;
    requires = ListOf String;
  };
in
  AspectDecl.check {
    name = "workspace-shell";
    target = "module";
    requires = [ "toolchain" ];
  }

The check is structural and derived. Each field is checked with its own type, and the composed type preserves enough context for diagnostics to point at the field that failed. Adding another field or nesting another record changes the type description; the validator follows automatically.

Dependent records

Some fields depend on earlier fields. DepRecord evaluates field types left to right, so later field types can inspect earlier values:

let
  inherit (fx.types) Bool String ListOf DepRecord refined;

  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  AspectDecl = DepRecord [
    { name = "generated"; type = Bool; }
    { name = "target"; type = self:
        if self.generated then TargetClass else String; }
    { name = "requires"; type = _: ListOf String; }
  ];
in {
  ok = AspectDecl.checkFlat {
    generated = true;
    target = "module";
    requires = [ "toolchain" ];
  };

  bad = AspectDecl.checkFlat {
    generated = true;
    target = "fleet";
    requires = [ ];
  };
}

The dependent field type is never evaluated until the fields it depends on have passed. That ordering keeps diagnostics local and avoids running domain logic on malformed input.

Check vs validate

Use .check when you need a boolean:

AspectDecl.checkFlat value

Use .validate when the caller needs diagnostics:

fx.run (AspectDecl.validate value)
  fx.effects.typecheck.collecting []

The validation path reports through effects, so choosing a handler chooses policy. A CLI can collect every field error. CI can abort on the first fatal error. Tests can inspect the emitted diagnostics as data.

This separates two concerns that are often mixed together in Nix DSLs: the type describes the accepted shape, while the handler decides whether a failed check becomes an exception, a list of diagnostics, or a trace.

Where the kernel fits

Every public type carries a kernel representation. Primitive and first-order types can use fast decidable checks. Higher-order and proof oriented boundaries use HOAS terms that the kernel checks directly.

This is one model, not two. Value-level validation is the practical entry point; generated datatypes and verified functions reuse the same kernel-backed structure when the boundary needs more evidence than a predicate can provide.