nix-effects

nix-effects provides composable, handler-driven effects via a freer monad with O(1) bind, a dependent type checker grounded in MLTT, and stack-safe evaluation via trampolining — all implemented entirely in pure Nix.

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
• Proof Guide - a first introduction to writing proofs for the nix-effects type checker
• 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.