nix-effects
A type-checking kernel, algebraic effects, and dependent types in pure Nix.
A proof-checking kernel, algebraic effects, and dependent types, implemented in pure Nix.
nix-effects brings ideas from type theory and functional programming to the Nix ecosystem: a verified type-checking kernel with dependent types, an algebraic effect system for composable side effects, and stack-safe evaluation via trampolining.
Guide
The guide walks through nix-effects from first principles:
- Introduction — what nix-effects is and why it exists
- Getting Started — installation, first program, REPL workflow
- Theory — algebraic effects, handlers, and the mathematical foundations
- 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
API Reference
Auto-generated reference documentation covering the core API, effect handlers, type constructors, stream combinators, and the type-checker internals.