Guide
A practical path through nix-effects: start with imports and handlers, then move into typed validation, generated datatypes, ornaments, proofs, and syntax su...
The guide is the shortest path from using nix-effects to understanding the pieces that make it useful. Start with setup and handler basics, then follow the later chapters when you need typed validation, description-backed datatypes, ornaments, proofs, or syntax helpers.
Introduction
nix-effects is a typed, description-backed programming substrate for pure Nix that runs every check at nix eval time before anything builds.
Getting Started
Install nix-effects as a flake input or direct import, define a first type with fx.types, and run a computation through fx.run with a handler.
Effects and Handlers
Algebraic effects (send/bind/pure plus handlers) separate program intent from execution policy; the substrate underlies fx.types, diagnostics, and the checker.
Typed Validation
fx.types wraps Nix value predicates with kernel-backed type information; refinements layer guard predicates over structural checks via fx.refine.
Generated Datatypes
H.datatype generates a Nix record whose constructors, type, and description are reusable by the checker, generic walkers, schemas, and ornaments.
Generic Programming
fx.types.generic consumes the levitated Desc of generated datatypes so checker, derive, and schema agree by sharing one metadata tree per type.
Ornaments and Description-Backed Data
Ornaments refine one generated datatype into another while preserving a forgetful map back, so enriched values stay usable wherever the base value fit.
Proof Guide
Build proofs in nix-effects from Refl through the J eliminator to verified extraction of plain Nix functions from kernel-checked HOAS terms via NbE.
Sugar
fx.sugar adds opt-in syntax (do, /, steps, letM, with, wrap) over the effect substrate; the kernel never imports it and removing it changes nothing.