kleisli-io/nix-effects

---

kleisli-io/nix-effects.json

{
  "createdAt": "2026-02-21T15:57:41Z",
  "defaultBranch": "main",
  "description": "Pure Nix effects, typed validation, verified boundaries, and description-backed DSLs",
  "fullName": "kleisli-io/nix-effects",
  "homepage": "https://docs.kleisli.io/nix-effects",
  "language": "Nix",
  "name": "nix-effects",
  "pushedAt": "2026-06-14T09:38:08Z",
  "stargazersCount": 37,
  "topics": [],
  "updatedAt": "2026-06-14T09:38:12Z",
  "url": "https://github.com/kleisli-io/nix-effects"
}

nix-effects

[]!(LICENSE)

A pure Nix toolkit for effectful programs, auto-derived validation, verified boundaries, and description-backed DSLs.

nix-effects hosts a small typed kernel inside Nix evaluation. That makes types and datatype descriptions inspectable Nix values, so validators, schemas, documentation, dependency extractors, and DSL interpreters can be derived from the same structure without an external schema language, compiler plugin, or macro system.

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

Everything runs at nix eval time.

Documentation

Small example

Validation is derived from type descriptions. You define the shape once; nix-effects derives the traversal, sends typeCheck at every field, branch, and list index, and leaves error policy to the handler:

let
  inherit (fx.types) Record ListOf String refined;

  TargetClass = refined "TargetClass" String
    (x: builtins.elem x [ "module" "file" "package" "check" ]);

  AspectDecl = Record {
    name = String;
    target = TargetClass;
    requires = ListOf String;
  };

  bad = {
    name = "workspace-aspect";
    target = "fleet";
    requires = [ "base" 1 ];
  };
in
  fx.handle {
    handlers = fx.effects.typecheck.collecting;
    state = [];
  } (AspectDecl.validate bad)

That single AspectDecl description produces checks for the record, the target refinement, and every element of requires. The user does not write a validator for the record. The handler only decides what to do with derived failures:

# src/effects/typecheck.nix — six policies for the same typeCheck effect.
strict = {
  typeCheck = { param, state }:
    if param.type.check param.value
    then { resume = true; inherit state; }
    else
      let reason = param.reason or "shape-mismatch"; in
      builtins.throw "[${reason}] ${mkMessage param}";
};

collecting = {
  typeCheck = { param, state }:
    if param.type.check param.value
    then { resume = true; inherit state; }
    else {
      resume = false;
      state = state ++ [ (mkErrorRecord param) ];
    };
};

logging = {
  typeCheck = { param, state }:
    let passed = param.type.check param.value;
    in {
      resume = passed;
      state = state ++ [{
        context = param.context;
        typeName = param.type.name;
        path = param.path or [ ];
        reason = param.reason or "shape-mismatch";
        inherit passed;
      }];
    };
};

firstN = N: { /* collect at most N mkErrorRecord failures */ };
summarize = { /* count passes/failures and group failures by reason */ };
pretty = cfg: { /* render "[reason] Expected T at <path>, got <shape>" */ };

The same derived validation runs under all six without a rewrite. strict throws on the first bad field. collecting visits every reachable position and returns { context, typeName, actual, path, reason, message } records. logging records every check, pass or fail. firstN keeps a bounded prefix of failures, summarize keeps aggregate counts by reason, and pretty stores display-ready diagnostic lines.

The dependent type checker is ordinary pure Nix, but the generated .validate route goes through the typeCheck effect, so type errors in deeply nested terms come back with the field, branch, or index path that broke.

Table of contents

• [Small example]!(#small-example)
• [What you can build]!(#what-you-can-build)
• [Core concepts]!(#core-concepts)
• [Quick start]!(#quick-start)
• [Effects]!(#effects)
• [Typed boundaries]!(#typed-boundaries)
• [Datatypes and descriptions]!(#datatypes-and-descriptions)
• [Streams and pipelines]!(#streams-and-pipelines)
• [Syntax sugar]!(#syntax-sugar)
• [API reference]!(#api-reference)
• [How it works]!(#how-it-works)
• [Known limitations]!(#known-limitations)
• [Testing]!(#testing)
• [Documentation MCP server]!(#documentation-mcp-server)
• [Formal foundations]!(#formal-foundations)
• [Used by]!(#used-by)
• [Acknowledgments]!(#acknowledgments)
• [License]!(#license)

What you can build

• Auto-derived validators. Every described type gets structural validation with exact blame paths. Users define shapes and refinements, not per-type traversals.
• Effectful pipelines. Model eval-time workflows with state, errors, scoped context, accumulation, nondeterminism, restarts, and streams.
• Description-backed DSLs. Define domain shapes once, then interpret them as derivations, descriptors, documentation, schemas, tests, graphs, or dashboards.
• Verified boundaries. Check proofs or implementations against kernel types before extracting ordinary Nix functions.
• Generic datatype tooling. Write consumers over datatype descriptions instead of repeating per-type traversal, schema, dependency, or validation code.

Core concepts

• Computations are freer-monad values. pure returns a value, send requests an effect, bind sequences work, and run interprets the tree.
• Handlers own operational policy. The same computation can abort, resume, collect errors, hide scoped state, or route unknown effects outward depending on the handler.
• Typed boundaries connect runtime Nix values to the MLTT kernel. Generic validation is derived for every described type, refinements add domain predicates, and verified HOAS terms can be extracted as plain Nix.
• Descriptions are reusable datatype shapes. The public inductive prelude and user datatypes share the same description-backed macro surface, so generic tools can inspect and consume datatype structure.
• Streams and pipelines are effectful programs too. They compose with the same bind, handler, and trampoline machinery as validation.

Examples in this repository

• Category theory library (examples/category-theory/) shows proofs, arithmetic, algebraic structures, functors, and Yoneda through the HOAS and datatype surface.
• Expression interpreter and build simulator (examples/interp/, examples/build-sim/) exercise the effect layer at scale.

Quick start

Add nix-effects as a flake input:

{
  inputs.nix-effects.url = "github:kleisli-io/nix-effects";

  outputs = { nix-effects, ... }:
    let fx = nix-effects.lib;
    in {
      # Use fx.types, fx.run, fx.send, fx.bind ...
    };
}

Or import directly (non-flake):

let
  pkgs = import <nixpkgs> {};
  fx = import ./path/to/nix-effects { lib = pkgs.lib; };
in ...

Effects

An effectful computation is a freer monad value: a tree of effects with continuations. send creates an effect. bind sequences computations. run interprets the tree through a handler.

# A computation that reads state, doubles it, writes it back
comp = bind get (s:
  bind (put (s * 2)) (_:
    pure s));

# Run with state handler
result = fx.run comp {
  get  = { param, state }: { resume = state; inherit state; };
  put  = { param, state }: { resume = null; state = param; };
} 21;

# result.value = 21, result.state = 42

Same computation, different handler

Define the type once. Swap the handler to change error policy.

validation = AspectDecl.validate {
  name = "workspace-aspect";
  target = "fleet";
  requires = [ "base" 1 ];
};

# Strict — throw on first error
strict = fx.run validation fx.effects.typecheck.strict null;

# Collecting — gather every reachable error record
collecting = fx.run validation fx.effects.typecheck.collecting [];

# Summary — bounded state for large validations
summary = fx.run validation fx.effects.typecheck.summarize {
  byReason = {};
  passed = 0;
  failed = 0;
};

The resume vs abort distinction: resume feeds a value back to the continuation and keeps running. abort discards the continuation and returns immediately. Handlers should return one of { resume = value; state = ...; } or { abort = value; state = ...; }. If both are present, abort takes priority.

Built-in effects

Module	Operations	Purpose
state	get, put, modify, gets	Mutable state
error	raise, raiseWith	Error handling
reader	ask, asks, local	Read-only environment
writer	tell, tellAll	Append-only log
acc	emit, emitAll, collect	Value accumulation
choice	choose, fail, guard	Nondeterminism
conditions	signal, warn	Common Lisp-style restarts
typecheck	sent by derived validation	Type validation with blame
linear	acquire, consume, release	Graded linear resource tracking
scope	run, runWith, stateful, provide, val	Scoped handlers
hasHandler	hasHandler	Runtime handler presence check

Typed boundaries

Every type is grounded in an MLTT type-checking kernel. The structural guard (check) is derived from the kernel’s decide procedure. The verifier (validate) is generated from the type description and sends typeCheck effects through the freer monad for blame tracking. You choose the error policy by choosing the handler.

First-order types

fx.types.String   fx.types.Int    fx.types.Bool
fx.types.Float    fx.types.Attrs  fx.types.Path
fx.types.Function fx.types.Null   fx.types.Unit  fx.types.Any

Each wraps a builtins.is* check:

fx.types.String.check "hello"  # true
fx.types.Int.check "hello"     # false

Constructors

Build compound types from simpler ones:

# Record with typed fields (open — extra fields allowed)
PersonT = Record { name = String; age = Int; };
PersonT.check { name = "Alice"; age = 30; }  # true

# Homogeneous list
(ListOf Int).check [ 1 2 3 ]  # true

# Optional value
(Maybe String).check null     # true
(Maybe String).check "hello"  # true

# Tagged union (two branches)
(Either Int String).check { _tag = "Left"; value = 42; }   # true

# Tagged union (open)
(Variant { circle = Float; rect = Attrs; }).check { _tag = "circle"; value = 5.0; }  # true

The generic validator derives the descent for every constructor. ListOf emits indexed positions, Record emits field positions, and Variant emits branch positions. Nested records, lists, and variants compose without user-written validator code.

Refinement types

Narrow any type with a predicate (Freeman & Pfenning 1991; cf. Rondon et al. 2008):

Nat = refined "Nat" Int (x: x >= 0);
TargetClass = refined "TargetClass" String
  (x: builtins.elem x [ "module" "file" "package" "check" ]);
NonEmpty = refined "NonEmptyString" String (s: builtins.stringLength s > 0);

# Predicate combinators
refined "Safe" String (allOf [ (s: s != "") (s: !(builtins.elem s blocked)) ])
refined "Either" Int (anyOf [ (x: x < 0) (x: x > 100) ])

Built-in refinements: positive, nonNegative, inRange, nonEmpty, matching.

Refinements do not require hand-written structural validation. The generic validator checks the underlying type first, then runs the domain predicate and reports a predicate failure at the same derived path.

Dependent and proof terms

Pi encodes dependent functions, Sigma dependent pairs, and DepRecord dependent records. Identity types expose Refl and J; sym, trans, cong, and transport are derived from J.

fx.types.hoas builds proof terms. fx.types.extract and verifyAndExtract check a HOAS body at the boundary and return an ordinary Nix callable when verification succeeds.

Universe levels

Types themselves have types, stratified to prevent accidental paradoxes. The kernel is non-cumulative: moving data across universe levels is explicit via LiftAt, liftAt, and lowerAt:

Type_0  # Type of value types (Int, String, ...)
Type_1  # Type of Type_0
Type_2  # Type of Type_1
# typeAt n works for any n; Type_0 through Type_4 are convenience aliases.
# 4 is arbitrary; most description-backed DSLs stay near Type_0 or Type_1.

(typeAt 0).check Int    # true — Int lives at universe 0
level Int               # 0

For kernel-backed types, levels are computed from the typing derivation. Transport across levels is represented in the term language instead of hidden behind cumulative subtyping.

Usage-checked values

Linear, Affine, and Graded types track resource usage with exact, bounded, or graded counts.

Datatypes and descriptions

Descriptions are reusable datatype shapes. Desc and μ provide the generic induction boundary; the public inductive prelude (Nat, List, Sum, Bool, Eq, Fin, Vec, W) and user-defined datatypes share the same description-backed macro surface.

The datatype macro lets you declare single- or multi-constructor datatypes directly in HOAS with datatype, datatypeP, datatypeI, datatypePI, conI, field, fieldD, piField, piFieldD, recField, and recFieldAt. Dependent fields see prior fields by name (prev.op, prev.comp), parameters thread through a paramPi binder, and indexed families can compute their target index.

Generic programs consume those descriptions. The same shape can derive a schema, documentation, dependencies, folds, value views, and validation. The validation derivation is the important boundary: every described type gets a checker from its structure, including user datatypes that did not exist when nix-effects was written.

Chains of saturated or linear-recursive constructors flatten to flat desc-con terms at elaboration time, so deeply nested generated lists and natural numbers remain stack-safe.

The category theory library in [examples/category-theory/]!(examples/category-theory/) uses the same surface for arithmetic proofs, algebraic structures, functors, and Yoneda’s lemma.

Streams and pipelines

Effectful lazy sequences. Each step yields Done (finished) or More (element + continuation):

# Generate, transform, consume
result = fx.run
  (fold (a: b: a + b) 0 (take 5 (map (x: x * x) (range 1 100))))
  {} null;
# result.value = 55 (1² + 2² + 3² + 4² + 5²)

Available: fromList, iterate, range, replicate, map, flatMap, filter, scanl, take, takeWhile, drop, fold, toList, length, sum, signal, signalOn, any, all, concat, interleave, zip, zipWith.

Syntax sugar

fx.sugar is an opt-in syntax layer. do and letM replace nested bind chains; __div (behind fx.sugar.operators) lets you write a / f / g for left-associative bind pipelines; fx.sugar.types pre-wraps the zero-ary primitives with a __functor that applies a predicate via fx.types.refined. The kernel doesn’t import any of it. See [book/src/sugar.md]!(book/src/sugar.md) for usage forms, caveats, and forward-compatibility notes.

API reference

The fx attrset exposes the public API. Common entry points:

fx.pure                              fx.impure                            fx.isPure
fx.isComp                            fx.match                             fx.send
fx.bind                              fx.map                               fx.seq
fx.pipe                              fx.kleisli                           fx.run
fx.handle                            fx.rotate                            fx.queue
fx.adapt                             fx.adaptHandlers

fx.types.mkType                      fx.types.check                       fx.types.validate
fx.types.make                        fx.types.refine                      fx.types.defEq

fx.types.String                      fx.types.Int                         fx.types.Bool
fx.types.Float                       fx.types.Attrs                       fx.types.Path
fx.types.Derivation                  fx.types.Function                    fx.types.Null
fx.types.Unit                        fx.types.Any

fx.types.Record                      fx.types.ListOf                      fx.types.Maybe
fx.types.Either                      fx.types.Variant

fx.types.Pi                          fx.types.Sigma                       fx.types.Certified
fx.types.Vector                      fx.types.DepRecord

fx.types.Linear                      fx.types.Affine                      fx.types.Graded

fx.types.refined                     fx.types.allOf                       fx.types.anyOf
fx.types.negate                      fx.types.positive                    fx.types.nonNegative
fx.types.inRange                     fx.types.nonEmpty                    fx.types.matching

fx.types.typeAt                      fx.types.level
fx.types.Type_0 .. fx.types.Type_4   # convenience aliases; typeAt n works for any n

fx.effects.get                       fx.effects.put                       fx.effects.modify
fx.effects.gets                      fx.effects.state                     fx.effects.error
fx.effects.typecheck                 fx.effects.policy                    # alias for fx.effects.typecheck.policy
fx.effects.conditions                fx.effects.reader                    fx.effects.writer
fx.effects.acc                       fx.effects.choice                    fx.effects.linear
fx.effects.scope                     fx.effects.hasHandler

fx.stream.done                       fx.stream.more                       fx.stream.fromList
fx.stream.iterate                    fx.stream.range                      fx.stream.replicate
fx.stream.map                        fx.stream.flatMap                    fx.stream.filter
fx.stream.scanl                      fx.stream.take                       fx.stream.takeWhile
fx.stream.drop                       fx.stream.fold                       fx.stream.toList
fx.stream.length                     fx.stream.sum                        fx.stream.signal
fx.stream.signalOn                   fx.stream.any                        fx.stream.all
fx.stream.concat                     fx.stream.interleave                 fx.stream.zip
fx.stream.zipWith

fx.types.hoas                        fx.types.verified
fx.types.elaborateType               fx.types.elaborateValue              fx.types.validateValue
fx.types.extract                     fx.types.extractInner                fx.types.reifyType
fx.types.verifyAndExtract            fx.types.decide                      fx.types.decideType
fx.types.generic.check.deriveCheck   fx.types.generic.check.checkWithGuard
fx.types.generic.derive.deriveSchema fx.types.generic.derive.deriveDocs
fx.types.generic.derive.deriveDeps   fx.types.generic.value.view

fx.kernel.pure                       fx.kernel.send                       fx.kernel.bind
fx.kernel.pipe                       fx.kernel.kleisli
fx.trampoline.handle

fx.sugar.do                          fx.sugar.letM                        fx.sugar.operators.__div
fx.sugar.types.wrap                  fx.sugar.types.Int                   fx.sugar.types.String
fx.sugar.types.Bool                  fx.sugar.types.Float                 fx.sugar.types.Path
fx.sugar.types.Null                  fx.sugar.types.Unit                  fx.sugar.types.Any

Types additionally expose:

T.check v          -- decide via kernel (elaborate + type-check)
T.prove term       -- verify a HOAS proof term against the kernel type
T._kernel          -- the kernel type (HOAS tree)

How it works

Computations are freer monad values: Pure value or Impure effect continuation, constructed via comp.pure and comp.impure (the comp module is the single source of truth for the Computation ADT). bind appends to an FTCQueue (catenable queue) in O(1). send uses an Identity queue sentinel so the trampoline can skip the identity continuation application entirely.

The interpreter uses builtins.genericClosure — Nix’s only iterative primitive — as a trampoline, giving O(1) stack depth for the main dispatch loop. Each step calls the handler for the current effect, processes the continuation queue inline via recursive applyQueue, and produces the next computation node — one genericClosure step per effect. deepSeq on the handler state in the key field breaks thunk chains that would otherwise blow memory. Test suite validates 100,000 operations; deep pure bind chains use the iterative queue path.

Known limitations

Certified carries a boolean witness, not an inhabitation proof. Certified(A, P) = Σ(v:A).{p : Bool | p ∧ P(v)} stores the boolean result of P(v) as its second component rather than a term inhabiting P(v). Predicate evaluation happens at construction time and produces no transportable proof term. For genuinely propositional content, use Pi with identity types and the J-derived combinators (sym, trans, cong, transport) from fx.types.hoas.

Universe levels are partially enforced. For kernel-backed types, checkTypeLevel computes the correct universe level from the typing derivation. For non-kernel types, the universe field remains a trusted declaration — nothing prevents a user from declaring universe = 0 on a type that operates at a higher level. Computing sup_{a:A} level(B(a)) for arbitrary type families requires evaluating on all domain values, which is undecidable. The hierarchy prevents accidental paradoxes; the kernel enforces it for types it knows about.

Effects are string-keyed, not extensible. Kiselyov & Ishii (2015) contributes both the freer monad encoding with FTCQueue and extensible effects via open unions. nix-effects implements the first but not the second. Effect handlers go into a single flat attrset per run call; name collisions are silently accepted (last handler wins via attrset merge).

O(1) stack depth caveat. The trampoline gives O(1) stack for the main dispatch loop. Continuation queue application is inlined as a recursive function (depth-limited to 500) with a genericClosure fallback for deep pure chains, so chains of 10,000+ pure binds are handled iteratively. Queue rotation (viewlGo) uses genericClosure for deep left-nested trees. The remaining stack risk is in user-supplied handler functions that recurse deeply within a single trampoline step.

Handler state must be deepSeq-safe. The trampoline uses builtins.deepSeq on handler state at each step to break thunk chains. This means handler state must not contain functions (closures), since deepSeq on a function is a no-op in Nix — thunks captured inside closures survive the eager evaluation and can accumulate. All built-in handlers use scalar or flat-attrset state (safe). Custom handlers with closure-valued state may lose the thunk-breaking guarantee.

Testing

# Run all tests via nix-unit (flake)
nix flake check

# Run all tests via nix-unit (non-flake)
nix-unit ./tests.nix

# Inspect the generated nix-unit tree
nix eval --impure --expr \
  'let fx = import ./. { lib = (builtins.getFlake "nixpkgs").lib; };
   in builtins.attrNames fx.tests.nix-unit.integration'

Tests cover algebraic laws (functor, monad), all type constructors including dependent and linear types, the trampoline at 100k operations, error paths, streams, and HOAS proof verification.

Documentation MCP server

The full nix-effects manual is published at https://docs.kleisli.io/nix-effects, and an MCP (Model Context Protocol) server lets AI agents search and fetch it programmatically.

• Explainer: https://docs.kleisli.io/mcp (human-readable; lists tools, resources, and copy-pasteable client configs).
• Transport endpoint: https://docs.kleisli.io/mcp/transport (Streamable HTTP per spec 2025-03-26 — POST/GET/DELETE).
• Tools: search_docs(query), get_page(project, section, page), list_projects().
• Resources: docs://kleisli/{project}/{section}/{page}.

Diag hints (fx.diag.hints.hints) carry a docLink field pointing at a per-key heading anchor on the diag module page, so AI tooling that surfaces hints can deep-link directly to the relevant prose.

Markdown affordances

Every doc page is also available as raw Markdown — useful for token-efficient agent consumption:

• Append .md to any path: …/nix-effects.md, …/nix-effects/core-api.md, …/nix-effects/diag/hints.md.
• Or send Accept: text/markdown on the original path; the server returns Content-Type: text/markdown instead of HTML.
• Doc pages emit a Link: <{path}.md>; rel="llms-txt-page" response header pointing at the markdown alternate.

Connecting from Claude Code

Add the server to ~/.claude/mcp.json (or per-project .claude/mcp.json):

{
  "mcpServers": {
    "kleisli-docs": {
      "type": "http",
      "url": "https://docs.kleisli.io/mcp/transport"
    }
  }
}

Tools then surface as mcp__kleisli-docs__search_docs, mcp__kleisli-docs__get_page, mcp__kleisli-docs__list_projects.

For Cursor and generic JSON-RPC client configs, see https://docs.kleisli.io/mcp.

Formal foundations

Key papers that shaped the design:

• Martin-Löf (1984) Intuitionistic Type Theory. Pi, Sigma, universe hierarchy. nix-effects implements these in an MLTT type-checking kernel (src/tc/) — all types are grounded in the kernel, which operates at nix eval time.

• Findler & Felleisen (2002) Contracts for Higher-Order Functions. The guard/verifier decomposition follows their strategy: first-order types check immediately, higher-order types (Pi) defer to elimination.

• Freeman & Pfenning (1991) Refinement Types for ML. The concept of narrowing a type with a predicate. nix-effects’ refined constructor and predicate combinators implement runtime refinement checking. Rondon, Kawaguchi & Jhala (2008) extended this with SMT-based inference (Liquid Types); nix-effects uses predicates rather than SMT solvers.

• Plotkin & Pretnar (2009) Handlers of Algebraic Effects. The handler pattern. resume invokes the continuation, abort discards it.

• Kiselyov & Ishii (2015) Freer Monads, More Extensible Effects. The freer monad encoding and FTCQueue (catenable queue) that give O(1) bind and make effectful validation practical at scale. nix-effects uses the freer encoding and FTCQueue but does not implement the paper’s extensible effects (open unions, Member constraint).

• Orchard, Liepelt & Eades (2019) Quantitative Program Reasoning with Graded Modal Types. The graded linear type model. nix-effects’ Linear, Affine, and Graded types implement resource-usage tracking following this quantitative framework.

Used by

Projects that import nix-effects as a dependency. If your project uses nix-effects and you’d like it listed here, open a PR.

• den by @vic — an aspect-oriented Nix configuration framework. Den uses nix-effects at its core to achieve dependency injection via effect-rotation and scoped-handlers. Den configuration pipeline uses effect-handlers for keeping module-provenance and dedup, dependency-tracing, fleet-graphs, custom Nix classes forwarding, cross-host or cross-aspect configurations, and other advanced features.

• ned by @vic — Ned is a minimalist kernel built upon nix-effects to bring effectful stream-based Functional-Reactive-Programming into Nix. Ned was born from the experience and knowledge obtained while using nix-effects in Den. Ned is being used to simplify Den’s internal subsystems communication and effect-protocols by using cycle-like composition while keeping effects drive state and events.

• dnzl by @vic — Dnzl is an Actor System for Nix based using nix-effects streams for inbox and sidecar communication channels. Behaviours are plain Nix functions that become actors when incoming messages are stream-folded over state. Dnzl features idiomatic behaviour replacement, state and error handling. Dnzl actors are based on Ned cycles for composability, creating trees of nested actors ala erlang.

• zen by @vic — Zen is a minimal stream-based Nix module system. It uses nix-effects rotation and scoped handlers to achieve sub-modules and provide the config fixed-point via Ned streams. It also aims to provide other advanced features made possible by nix-effects: Inter module communication -akin to Actors- where modules can query others without knowing about their names (decoupling), negotiate merge strategies, reconciliate on values by interested modules, stateful mediators, etc. Zen aims to use nix-effect’s MLTT types for verification, and allow only proved configs to be created.

Acknowledgments

nfx by Victor Borja (Apache-2.0) shaped the API design of this project. The adapt handler combinator, the mk { doc, value, tests } structured module pattern, and the effect module vocabulary (state, acc, conditions, choice, streams) all come from nfx. nix-effects builds a different core on freer monads with FTCQueue (Kiselyov & Ishii 2015) and adds a type-checking kernel and dependent type system that nfx does not attempt, but the overall API owes a clear debt to that project.

License

[MIT]!(LICENSE)