Guide
8 pages
Introduction
Nix configurations fail late. A misspelled option name, a string where an
integer belongs, a firewall rule that...
Getting Started
Installation
Add nix-effects as a flake input:
{
inputs.nix-effects.url = "github:kleisli-io/nix-effects";
...
Proof Guide
Nix configurations are concrete at eval time. Every field, every value,
every list element is known before anything...
Theory
Nine papers shaped nix-effects. Here's how each one maps to code.
Algebraic effects and the freer monad
A computation...
Trampoline
The trampoline is how nix-effects interprets freer monad computations
with O(1) stack depth in a language with no...
Systems Architecture
nix-effects is a freer-monad effect layer with a dependent type checker
on top, all running at nix eval time. The...
Kernel Architecture
This chapter describes the type-checking kernel: its pipeline, its
primitives, and how to write verified...
Kernel Formal Specification
This document is the contract the implementation must satisfy. Every
typing rule, compute rule, and conversion rule is...