nix-effects

nix-effects provides effectful programs, typed validation, verified boundaries, and description-backed DSLs entirely in pure Nix.

Programs describe what they need. Handlers decide policy. Types, datatypes, and proofs describe the structure that generic tools can validate, interpret, extract, or document.

Guide

The guide walks through nix-effects from first principles:

• Introduction — what nix-effects is and why it exists
• Getting Started — installation, first type, first effect, first generated datatype
• Effects and Handlers — computations describe operations; handlers choose policy
• Typed Validation — primitive, refined, structured, and dependent validation boundaries
• Generated Datatypes — descriptions, constructors, metadata, and generated families
• Generic Programming — derive schemas, dependency graphs, diagnostics, and structural views
• Ornaments and Description-Backed Data — enrich generated datatypes while preserving forgetful maps
• Proof Guide — a first introduction to writing proofs for the nix-effects type checker
• Sugar — opt-in syntax for effect pipelines and refined types

Concepts

Concept chapters explain the ideas behind the programming model:

• Theory — algebraic effects, handlers, MLTT, descriptions, and the mathematical foundations

Internals

Implementation chapters are grouped for contributors:

• Trampoline — stack-safe evaluation and the trampoline machine
• Systems Architecture — how the components fit together
• Kernel Architecture — the MLTT type-checking kernel internals
• Kernel Specification — formal specification with typing rules

Examples

Examples show complete uses of nix-effects in small programs. The source lives under examples/ if you want to run or adapt it locally:

• Overview — where to start and where the source lives
• Proofs — computational proofs, equality combinators, and verified functions
• Effects and Validation — one validation computation under collecting, logging, and strict handlers
• Surface Languages — STLC surface syntax, products, sums, recursive lists, refinements, and diagnostics

API Reference

Auto-generated reference documentation covering the core API, effect handlers, type constructors, stream combinators, and the type-checker internals.