# Kleisli.IO Documentation

> Documentation for Kleisli.IO — correctness infrastructure for the agentic era: formal methods, type theory, and Nix. Its flagship is kli, a radically extensible coding agent you run in your terminal and rewrite while it runs.

Kleisli.IO publishes four projects. You pose a "what if" to kli and it makes the change live instantly — even rewriting the running program itself; the other projects are the typed, verified Nix layer beneath it. Each project below is indexed by its sections, one line per page. Every page is also fetchable as Markdown — append `.md` to any URL or send `Accept: text/markdown` — and per-project (`/{project}/llms.txt`) and per-track (`/{project}/{track}/llms.txt`) indices keep context budgets small. Programmatic access (MCP) and the full discovery-affordance map are listed at the end.

## kli

kli is a radically extensible coding agent you rewrite while it runs.

### Learn

#### Get started

- [Teaching kli Your Project](https://docs.kleisli.io/kli/get-started/teaching-kli-your-project): Write an AGENTS.md that kli reads into its system prompt at startup, so it answers from your conventions instead of guessing or re-reading the tree.

#### Guides

- [Choose and Switch Models](https://docs.kleisli.io/kli/guides/choose-and-switch-models): Switch the running model with /model, list what is available with /models and /providers, set reasoning effort, and pin defaults in settings.json.
- [Connect a Provider](https://docs.kleisli.io/kli/guides/connect-a-provider): Authenticate a model provider in kli with /auth: reference an env var, store an API key, or run an OAuth login by pasting back the code.
- [Add a Custom OpenAI-Compatible Provider](https://docs.kleisli.io/kli/guides/add-a-custom-openai-compatible-provider): Point kli at a local or self-hosted OpenAI-compatible endpoint via providers.json: endpoint fields, semantic options, and model entries.
- [Run Commands and Eval Lisp](https://docs.kleisli.io/kli/guides/run-commands-and-eval-lisp): Run shell commands with the bash tool and evaluate Common Lisp in kli's live image with eval, including timeouts, output caps, and refused commands.
- [Persist and Resume Sessions](https://docs.kleisli.io/kli/guides/persist-and-resume-sessions): Make kli sessions durable with sessionDir, reopen them with /resume or the -c flag, and branch or step back through past turns with /branches and /rewind.
- [Manage Long Conversations](https://docs.kleisli.io/kli/guides/manage-long-conversations): Compact a kli session on demand with /compact, rely on automatic compaction as usage nears the model's context window, and label sessions with /name.
- [Inspect and Edit Context](https://docs.kleisli.io/kli/guides/inspect-and-edit-context): View what the model sees with /context inspect, stage append, remove, and replace edits, diff the pending set, then commit or revert them.
- [Steer a Running Turn](https://docs.kleisli.io/kli/guides/steer-a-running-turn): Redirect kli mid-run: steer at the next tool boundary, queue a follow-up for after the turn, tune steeringMode and followUpMode, and abort with Esc.
- [Restrict What kli Can Do](https://docs.kleisli.io/kli/guides/restrict-what-kli-can-do): Limit which tools kli may run by setting the capabilities array in settings.json; an empty array denies every gated tool, an absent key allows all.
- [Work in the TUI](https://docs.kleisli.io/kli/guides/work-in-the-tui): Drive the kli terminal interface: the keys you need, @file and $skill completion with Tab, the Ctrl+O tool-output toggle, and pinning a theme.
- [Run kli Headless or Piped](https://docs.kleisli.io/kli/guides/run-kli-headless-or-piped): Feed prompts to kli over a pipe with the non-tty line loop, one turn per line, and pick the headless or autonomous boot profile for unattended runs.
- [Switch and Customize Profiles](https://docs.kleisli.io/kli/guides/switch-and-customize-profiles): Pick a kli profile with --profile or KLI_PROFILE, switch live with /profile, and define your own in the profiles block of settings.json.
- [Update kli](https://docs.kleisli.io/kli/guides/update-kli): Run kli update to fetch the latest release, pin a version with --version, skip the prompt with --yes, and roll back automatically on a bad binary.
- [Log Observability Events](https://docs.kleisli.io/kli/guides/log-observability-events): Log kli's session events to a JSONL file by setting observability.path, scoping with observability.events, and checking the sink with /observability.

#### Concepts

- [The Live Image](https://docs.kleisli.io/kli/concepts/the-live-image): kli is a small kernel; every model provider, tool, command, and the terminal UI is a retractable extension you can add, change, or remove while it runs.
- [Extensions All the Way Down](https://docs.kleisli.io/kli/concepts/extensions-all-the-way-down): The mechanism said once: kli is a live image whose extension system is itself a retractable protocol. The spine, then the three pillars it buys you.
- [The Agent Loop](https://docs.kleisli.io/kli/concepts/the-agent-loop): How one kli turn seals a context snapshot, streams the model reply, runs tool calls serially, logs every result, and loops until the model stops asking.
- [Sessions as a Tree](https://docs.kleisli.io/kli/concepts/sessions-as-a-tree): Why a kli session is an append-only tree of parent-linked entries, what branches, rewind, and compaction summaries buy you, and why persistence is opt-in.
- [Context and the System Prompt](https://docs.kleisli.io/kli/concepts/context-and-the-system-prompt): How kli turns AGENTS.md, CLAUDE.md, SYSTEM.md, and APPEND_SYSTEM.md into the system prompt the model reads, with the discovery walk and the 2 MiB cap.
- [Tools and Hashline Edits](https://docs.kleisli.io/kli/concepts/tools-and-hashline-edits): How kli reads files with line anchors and edits them as anchor-validated patches that reject a stale or unread file instead of overwriting it.
- [Capabilities and Fault Barriers](https://docs.kleisli.io/kli/concepts/capabilities-and-fault-barriers): Why kli runs fully permissioned with no approval prompt, how the capabilities array restricts a session, and how barriers contain a fault.
- [Security Model and Sandboxing](https://docs.kleisli.io/kli/concepts/security-model-and-sandboxing): kli decides which capabilities an agent may exercise but never isolates its own process; for autonomous use you run kli inside a sandbox you control.
- [Profiles](https://docs.kleisli.io/kli/concepts/profiles): A profile is a named group of extension manifests that decides what kli boots with; pick one with --profile, KLI_PROFILE, or the profile settings key.
- [Models, Providers, and Transports](https://docs.kleisli.io/kli/concepts/models-providers-and-transports): kli splits a model registry, the providers that register models into it, and the transports that carry each API call, with auth set per provider.

### Extend

#### Extend kli

- [Choosing an Altitude](https://docs.kleisli.io/kli/extend/choosing-an-altitude): What each extension altitude can and cannot do: a Markdown slash command, a SKILL.md the model loads itself, or a Lisp extension that adds tools and behavior.
- [Prompt Templates](https://docs.kleisli.io/kli/extend/prompt-templates): A prompt template is a Markdown file whose name becomes a slash command and whose body is submitted as your message — the no-code way to extend kli.
- [Prompt Template Anatomy](https://docs.kleisli.io/kli/extend/prompt-templates/anatomy): How kli turns a prompts/*.md file into a slash command: the filename names it, frontmatter sets the hint, and the body becomes your user message.
- [Write Your First Prompt Template](https://docs.kleisli.io/kli/extend/prompt-templates/write-your-first): Create a prompts file in your project, start kli, and run it as a slash command. Your first kli customization with no code to write.
- [Using Arguments](https://docs.kleisli.io/kli/extend/prompt-templates/using-arguments): Pass arguments into a prompt template body: positional $1 and $2, the ${@:start:len} slice, $ARGUMENTS and $@ for all, and $RAW_ARGUMENTS.
- [Prompt Template Examples](https://docs.kleisli.io/kli/extend/prompt-templates/examples): Copy-paste prompt templates for code review, commit messages, and argument passing as complete files you drop into your kli prompts directory.
- [Skills](https://docs.kleisli.io/kli/extend/skills): A skill is a SKILL.md the model loads on its own when a task matches it, so kli picks up the right procedure without you naming a command first.
- [Skill Anatomy](https://docs.kleisli.io/kli/extend/skills/anatomy): A SKILL.md pairs a name with a required description the model reads to load the skill, plus the disable-model-invocation flag and a 2 MiB cap.
- [Write Your First Skill](https://docs.kleisli.io/kli/extend/skills/write-your-first): Author a SKILL.md the model auto-loads, then trigger it two ways: by its $name sigil and by letting its description match the task you describe.
- [Authoring and Discovery](https://docs.kleisli.io/kli/extend/skills/authoring-and-discovery): Place a skill where kli finds it, shadow a builtin by name, reference a skill with the $name sigil, and run one with the skill:name command.
- [Skill Examples](https://docs.kleisli.io/kli/extend/skills/examples): Four complete SKILL.md files to copy and adapt: a domain-knowledge skill, a tool recipe, a sigil-invoked skill, and one that shadows a built-in.
- [Lisp Extensions](https://docs.kleisli.io/kli/extend/lisp-extensions): A Lisp extension adds tools, slash commands, keybindings, themes, and renderers to kli, and lets you recode any one of them in place while the session runs.
- [Lisp Extension Anatomy](https://docs.kleisli.io/kli/extend/lisp-extensions/anatomy): How a kli extension is built: defextension yields a manifest thunk, install-manifest activates it as a recorded transaction, and every kind retracts.
- [Write Your First Lisp Extension](https://docs.kleisli.io/kli/extend/lisp-extensions/write-your-first): Author a single-file kli extension that adds a /greet slash command, load it, reload it live after an edit, and disable it without restarting.
- [Contribution Kinds](https://docs.kleisli.io/kli/extend/lisp-extensions/contribution-kinds): Contribute each kind from a kli extension with its retractor: a tool, slash command, event handler, keybinding, theme, status slot, or renderer.
- [Defining a Contribution Kind](https://docs.kleisli.io/kli/extend/lisp-extensions/defining-a-contribution-kind): Every contribution kind, including the kernel's own :tool, :method, and :theme, is defined with defcontribution-kind. Add one and defextension compiles it.
- [Recoding Live](https://docs.kleisli.io/kli/extend/lisp-extensions/recoding-live): Swap a whole extension with auto-rollback, hot-patch a behavior cell, and snapshot the protocol while kli runs, plus the capabilities each needs.
- [Loading and Managing Extensions](https://docs.kleisli.io/kli/extend/lisp-extensions/loading-and-managing): Load kli Lisp extensions from discovery dirs or --extension, set defaults in config.json, and toggle them live with /reload, /enable, /disable.
- [Lisp Extension Examples](https://docs.kleisli.io/kli/extend/lisp-extensions/examples): Five small, complete kli extensions in Common Lisp: a model tool, a slash command, a status-line widget, a theme, and a transcript message renderer.
- [Sharing Extensions](https://docs.kleisli.io/kli/extend/sharing-extensions): Install an extension someone published with kli install or /install: confirm two trust cards and pin the exact bytes to a git object id before any code loads.
- [Publishing Extensions](https://docs.kleisli.io/kli/extend/publishing-extensions): Package an extension as a single Lisp file or a directory bundle, pin it to a git object id, optionally sign it, and hand out the URL others install from.

### Reference

#### CLI & Install

- [Installation](https://docs.kleisli.io/kli/cli/installation): Install kli with the curl one-liner, the env vars that steer it, the on-disk layout, supported targets, and the Nix and from-source routes.
- [Environment Variables](https://docs.kleisli.io/kli/cli/environment-variables): Every environment variable kli and its installer read: provider keys, boot profile, docs origin, pinned version, install root, and download mirror.
- [Reading the Docs](https://docs.kleisli.io/kli/cli/docs): The `kli docs` subcommand: print kli documentation live as Markdown from docs.kleisli.io — the index, any page by its path, or a ranked search.

#### Commands, Tools & TUI

- [Slash Commands](https://docs.kleisli.io/kli/commands/slash-commands): Every kli slash command grouped by area, with the exact syntax and one-line effect for session, context, model, config, profile, and extension control.
- [Tools](https://docs.kleisli.io/kli/commands/tools): The agent tools in kli: bash, eval, read, find, search, write, and edit, with parameters, limits, hashline anchors, and capability gates.
- [Keymap](https://docs.kleisli.io/kli/commands/keymap): Every default key binding in the kli terminal UI, the action each one runs, and how to rebind keys with the keybindings setting in settings.json.
- [Themes](https://docs.kleisli.io/kli/commands/themes): The color token palette, the built-in dark and light themes, OSC 11 and COLORFGBG background detection, and pinning a theme in settings.json.

#### Settings & Files

- [settings.json](https://docs.kleisli.io/kli/config/settings): Every settings.json key for kli with type, default, and merge behavior, including model defaults, option settings, compaction, and fail-soft handling.
- [config.json](https://docs.kleisli.io/kli/config/config-json): The global config.json controls extension discovery with three keys: enabled, disabled, and extension-dirs. It is separate from settings.json.
- [The programs.kli Module](https://docs.kleisli.io/kli/config/nix-module): Bake extensions, settings, and sandboxing into a reproducible kli image with the programs.kli Home Manager and NixOS modules: options, wiring, and an example.
- [Capabilities](https://docs.kleisli.io/kli/config/capabilities): The capabilities that gate kli's tools, extension lifecycle, and credential reads, the implication rules, and how the settings array restricts them.
- [Profiles](https://docs.kleisli.io/kli/config/profiles): The four built-in kli profiles and their manifest groups and seams, the precedence that picks one at boot, and how to declare custom data profiles.
- [Files and Paths](https://docs.kleisli.io/kli/config/files-and-paths): Every path kli reads or writes: the global config and project directories, settings, credentials, providers, context files, sessions, and fault logs.

#### Models & Providers

- [Providers and Transports](https://docs.kleisli.io/kli/models/providers-and-transports): Reference for kli model providers (anthropic, openai, openai-codex, compatible), their wire transports, supported auth modes, and semantic options.

### Additional pages (including unstable internal surfaces)

- [CLI & Install](https://docs.kleisli.io/kli/cli/index): Reference for the kli program and its installer: argument dispatch, the subcommands and pass-through flags, the install one-liner, and supported targets.
- [Commands, Tools & TUI](https://docs.kleisli.io/kli/commands/index): Reference for driving kli inside a session: the slash-command catalogue, the agent tools, the default keymap, and the theme token palette.
- [Concepts](https://docs.kleisli.io/kli/concepts/index): Plain explanations of how kli works underneath: the agent loop, sessions, context, tools, the live image, permissions, profiles, models, and providers.
- [Settings & Files](https://docs.kleisli.io/kli/config/index): Reference for configuring kli: settings.json and config.json, how they deep-merge under a profile overlay, capabilities, profiles, and the paths kli touches.
- [Extend kli](https://docs.kleisli.io/kli/extend/index): kli is a live image: above a small boot kernel everything is an extension you install with a retractor, from a Markdown prompt to a method you rewrite live.
- [Get started](https://docs.kleisli.io/kli/get-started/index): Go from nothing to a running kli session, then the handful of things that are not like other agents: full permissions by default, and diffs already on disk.
- [Guides](https://docs.kleisli.io/kli/guides/index): Goal-named recipes for kli once it is running: switch models, connect a provider, resume a session, edit context, and restrict what it may touch.
- [Models & Providers](https://docs.kleisli.io/kli/models/index): The kli model catalogue across its providers: anthropic, openai, openai-codex, and user-defined compatible endpoints, with ids and context windows.

## cairn

cairn is a durable task graph your agent plans in and resumes into, keeping the plan outside the conversation so a context reset reloads it.

### Learn

#### Quickstart

- [Install cairn](https://docs.kleisli.io/cairn/get-started/install-cairn): Add cairn to kli declaratively or at runtime, then serve it to any MCP client so your agent can plan in and resume from a durable task graph.
- [Your first cairn session](https://docs.kleisli.io/cairn/get-started/your-first-cairn-session): Run the bootstrap-observe-handoff loop end to end: create a task, record an observation, scaffold a handoff, then resume the task from a clean session.
- [Plan and resume](https://docs.kleisli.io/cairn/get-started/plan-and-resume): Build a small phase graph with task_fork and task_link, ask the frontier what is ready, complete a phase, and resume the plan in a new session.

#### Concepts

- [What cairn is](https://docs.kleisli.io/cairn/concepts/what-cairn-is): cairn is continuity for agents: a durable, queryable task graph an agent plans into and resumes from, served over MCP and shipped as a kli extension.
- [The task graph](https://docs.kleisli.io/cairn/concepts/the-task-graph): How cairn keeps work in two stores: a directed, typed-edge graph of slug-addressed tasks and a full-text observation index, and what each edge means.
- [Tasks, observations, and handoffs](https://docs.kleisli.io/cairn/concepts/tasks-observations-handoffs): The three durable nouns of a cairn graph — the task node, the append-only observation heartbeat, and the resumable handoff whose summary is load-bearing.
- [Plans, phases, and the frontier](https://docs.kleisli.io/cairn/concepts/plans-phases-and-the-frontier): A plan in cairn is a task DAG, not a markdown file: phase-of children are phases, depends-on edges order them, and the frontier is the ready subset.
- [The current-task pointer](https://docs.kleisli.io/cairn/concepts/the-current-task-pointer): The current-task pointer is the per-session task cairn resolves slugless writes against and feeds each turn, moved by task_fork and task_bootstrap, not task_id.
- [Events, projection, and reconcile](https://docs.kleisli.io/cairn/concepts/events-projection-and-reconcile): How every cairn write appends one event to a durable per-task log, folds into a rebuildable SQLite projection, and reconciles the two on open.
- [Reads, writes, and capabilities](https://docs.kleisli.io/cairn/concepts/reads-writes-and-capabilities): How cairn separates reads from writes by capability rather than tool name, why the query language carries one dynamic write gate, and how a host enforces it.
- [The cairn-method](https://docs.kleisli.io/cairn/concepts/the-cairn-method): The cairn-method is the loop — research, plan, implement, validate — with observe and handoff as the heartbeat an agent uses to work a durable task graph.

### Reference

#### Tools & Query Language

- [MCP tools](https://docs.kleisli.io/cairn/reference/tools): The fourteen cairn MCP tools — one observe call, eight writes, five reads — each with its parameters, capability gate, returned text, and verbatim errors.
- [The TQ query language](https://docs.kleisli.io/cairn/reference/tq-language): TQ is the S-expression query language over the cairn task graph: sources, pipeline steps, predicates, set algebra, reflection, and the read-write gate.
- [Built-in and user-defined views](https://docs.kleisli.io/cairn/reference/views): The ten named views cairn ships, each with its exact TQ source text, plus how user-defined views shadow a built-in and how undefine restores it.
- [Edges, statuses, and fields](https://docs.kleisli.io/cairn/reference/edges-statuses-and-fields): The closed vocabularies of the cairn task graph: the three edge types, the five statuses, the eleven typed fields, and the reflective sources that list them.

#### Commands & Serving

- [Slash commands](https://docs.kleisli.io/cairn/cli/slash-commands): The six slash commands cairn registers under a kli host: observe, handoff, task, tasks, workon, where, with syntax, model visibility, and MCP analogue.
- [Serving over MCP](https://docs.kleisli.io/cairn/cli/mcp-serve): Reference for kli mcp-serve cairn: the MCP server command, its stdio invocation, and the surface it carries — fourteen tools, seven prompts, seven resources.

### Additional pages (including unstable internal surfaces)

- [Commands & Serving](https://docs.kleisli.io/cairn/cli/index): cairn's command-line surface: the six slash commands you type under a kli host, and serving cairn to any MCP client over stdio with kli mcp-serve.
- [Concepts](https://docs.kleisli.io/cairn/concepts/index): Plain explanations of how cairn works underneath: the task graph, observations and handoffs, plans and the frontier, the current pointer, and capabilities.
- [Quickstart](https://docs.kleisli.io/cairn/get-started/index): The cairn tutorial: install the extension, run the bootstrap-observe-handoff loop, then build a small phase graph you plan in and resume into.
- [Reference](https://docs.kleisli.io/cairn/reference/index): The precise surface of cairn: fourteen MCP tools, the TQ query language, the built-in views, and the closed edge, status, and field vocabularies.

## metaBuilder

Typed builder DSL built on nix-effects descriptions and internalized programs.

### Manual

- [Introduction](https://docs.kleisli.io/metaBuilder/manual/introduction): metaBuilder treats builders as typed descriptions, giving one build reusable validation, inspection, documentation, and materialization views.
- [Getting Started](https://docs.kleisli.io/metaBuilder/manual/getting-started): Define a small builder spec, construct a program, and run validate, dry-run, plan-view, introspect, and materialize.
- [Builder Specs](https://docs.kleisli.io/metaBuilder/manual/builder-specs): Builder specs name parameters, inputs, dependencies, tools, operations, outputs, and evidence before materialization.
- [Operations](https://docs.kleisli.io/metaBuilder/manual/operations): Operations describe build intent as data: read inputs, declare tools, write files, run commands, emit descriptors, and materialize.
- [Programs And Views](https://docs.kleisli.io/metaBuilder/manual/programs-and-views): The same builder program supports validation, dependency graph, dry-run, plan-view, describe, introspect, and materialization.
- [Designing Builder Surfaces](https://docs.kleisli.io/metaBuilder/manual/designing-builder-surfaces): Design builders from domain vocabulary first, then lower small public constructors into the shared metaBuilder program model.
- [Outputs, Evidence, And Runtime Artifacts](https://docs.kleisli.io/metaBuilder/manual/outputs-evidence-runtime): Outputs, descriptors, evidence, services, protocols, and runtime units describe what an artifact is and how it should run.
- [Materialization Model](https://docs.kleisli.io/metaBuilder/manual/materialization-model): Materialization interprets a builder program as a plan that produces derivations, outputs, and runtime declarations.
- [Authoring Production Builders](https://docs.kleisli.io/metaBuilder/manual/authoring-production-builders): Grow production builders from small domain constructors, explicit descriptors, standard views, and view-focused tests.

### Theory

- [Builders As Descriptions](https://docs.kleisli.io/metaBuilder/theory/builders-as-descriptions): A build description is structured data that can be checked, summarized, documented, interpreted, and materialized.
- [Internalized Programs](https://docs.kleisli.io/metaBuilder/theory/internalized-programs): Internalized programs represent build workflows as reusable values shared by validation, explanation, and materialization views.
- [Ornaments And Domain Surfaces](https://docs.kleisli.io/metaBuilder/theory/ornaments-and-domain-surfaces): Ornaments enrich the shared builder shape with domain-specific fields while preserving common interpretation behavior.
- [Interpretation And Views](https://docs.kleisli.io/metaBuilder/theory/interpretation-and-views): Each view is an interpretation of the same builder program: validation, graph, dry-run, plan, documentation, or artifact.
- [Evidence, Descriptors, And Runtime Structure](https://docs.kleisli.io/metaBuilder/theory/evidence-descriptors-runtime): Evidence, descriptors, services, protocols, and units belong in the descriptive model because artifacts have meaning beyond build success.

### Examples

- [Node service example](https://docs.kleisli.io/metaBuilder/examples/node-service): Guided Node service builder tour: runnable package, HTTP service descriptor, runtime unit, dependency graph, and materialization plan.
- [Source files](https://docs.kleisli.io/metaBuilder/examples/node-service/source): These files are the complete source for Node service example: the builder module plus the fixtures it consumes. Node...
- [Node service builder module](https://docs.kleisli.io/metaBuilder/examples/node-service/source/builder.nix): Source for the Node service builder constructor and worked demo program.
- [server.js](https://docs.kleisli.io/metaBuilder/examples/node-service/source/server.js): HTTP service fixture copied into the materialized Node demo package.
- [C code generation example](https://docs.kleisli.io/metaBuilder/examples/c-codegen): Guided C codegen builder tour: schema input, generated C sources, static library, CLI, descriptors, dependency graph, and materialization plan.
- [Source files](https://docs.kleisli.io/metaBuilder/examples/c-codegen/source): These files are the complete source for C code generation example: the builder module plus the fixtures it consumes. C...
- [C codegen builder module](https://docs.kleisli.io/metaBuilder/examples/c-codegen/source/builder.nix): Source for the C codegen builder constructor and worked native demo program.
- [messages.def](https://docs.kleisli.io/metaBuilder/examples/c-codegen/source/messages.def): Schema fixture consumed by the C code generator in the native demo.
- [main.c](https://docs.kleisli.io/metaBuilder/examples/c-codegen/source/main.c): Small CLI source linked against the generated static library.
- [Bridge example](https://docs.kleisli.io/metaBuilder/examples/bridge): Relates the shipped builder kinds — Node service, C code generation, OCI image, and IDL — through kernel-checked ornament, effect, and list-computation t...
- [Source files](https://docs.kleisli.io/metaBuilder/examples/bridge/source): These files are the complete source for Bridge example: the builder module plus the fixtures it consumes. Bridge proof...
- [Bridge proof module](https://docs.kleisli.io/metaBuilder/examples/bridge/source/bridge.nix): This module checks the bridge theorems and exposes their normal forms. Source path: examples/bridge.nix. nixcopyexpand{...
- [IDL example](https://docs.kleisli.io/metaBuilder/examples/idl): IDL example: multi-language protobuf code generation via the IdlBuilder ornament and internalized program interpreters.
- [Source files](https://docs.kleisli.io/metaBuilder/examples/idl/source): These files are the complete source for IDL example: the builder module plus the fixtures it consumes. IDL builder...
- [IDL builder module](https://docs.kleisli.io/metaBuilder/examples/idl/source/builder.nix): Source for the built-in IDL ornament demo and its worked program.
- [schema.proto](https://docs.kleisli.io/metaBuilder/examples/idl/source/schema.proto): This schema is the source artifact consumed by the IDL builder. The builder asks for C++ and Java generated views from...
- [OCI image example](https://docs.kleisli.io/metaBuilder/examples/oci-image): Guided OCI image builder tour: busybox layer, digest-chain assembly steps, image descriptor, smoke-test evidence, and materialization plan.
- [Source files](https://docs.kleisli.io/metaBuilder/examples/oci-image/source): These files are the complete source for OCI image example: the builder module plus the fixtures it consumes. OCI image...
- [OCI image example module](https://docs.kleisli.io/metaBuilder/examples/oci-image/source/builder.nix): Source for the worked busybox image spec and the exported views.

### API Reference

#### Core API

- [Descriptions](https://docs.kleisli.io/metaBuilder/core-api/descriptions): metaBuilder descriptions: generated datatypes for typed builder specifications and builder operations.
- [Operations](https://docs.kleisli.io/metaBuilder/core-api/operations): metaBuilder operations: smart constructors for typed builder and runtime operation records.

#### Program

- [Validate](https://docs.kleisli.io/metaBuilder/program/validate): validate: interprets builder programs into accumulated diagnostics.
- [Deps](https://docs.kleisli.io/metaBuilder/program/deps): deps: interprets builder programs into dependency and provenance graphs.
- [Dry-run](https://docs.kleisli.io/metaBuilder/program/dry-run): dry-run: interprets builder programs into operation summaries without materializing derivations.
- [Plan-view](https://docs.kleisli.io/metaBuilder/program/plan-view): plan-view: surfaces typed BuildPlan records and rendered shell commands without forcing derivations.
- [Describe](https://docs.kleisli.io/metaBuilder/program/describe): describe: interprets builder programs into a typed self-documentation model.
- [Introspect](https://docs.kleisli.io/metaBuilder/program/introspect): introspect: composed builder self-view over validation, deps, dry-run, plan-view, describe, and materialize.
- [Materialize](https://docs.kleisli.io/metaBuilder/program/materialize): materialize: lowers builder programs into typed BuildPlan records and runCommand derivations.
- [Backends](https://docs.kleisli.io/metaBuilder/program/backends): backends: plan translators that emit non-Nix build artifacts from a substrate-neutral BuildPlan.
- [Former](https://docs.kleisli.io/metaBuilder/program/former): former: derives a builder kind's op-coproduct side and state-ornament side from one argument tuple.
- [Plan-export](https://docs.kleisli.io/metaBuilder/program/plan-export): plan-export: serializes the pre-finalize PlanState to JSON with thunk-boxed derivation fields as the omission boundary.

#### Reference

- [Schemas](https://docs.kleisli.io/metaBuilder/reference/schemas): schema reference: JSON-schema artifacts derived from metaBuilder descriptions.
- [Datatypes](https://docs.kleisli.io/metaBuilder/reference/datatypes): datatype reference: descriptors for builder, runtime, and ornament vocabulary.

#### Ornaments

- [Project-builder](https://docs.kleisli.io/metaBuilder/ornaments/project-builder): ProjectBuilder ornament over BuilderSpec: super-base for project-level refinements (implementations, vendoring, testing). Inserts `langName` as the project's...
- [Dependencies](https://docs.kleisli.io/metaBuilder/ornaments/dependencies): DependenciesBuilder ornament over BuilderSpec: typed dependency-resolution strategy plus resolver eliminators. The 3-mode shape (Uniform / Partitioned / Mult...
- [Implementations](https://docs.kleisli.io/metaBuilder/ornaments/implementations): ImplementationsBuilder ornament over ProjectBuilder: typed multi-implementation refinement plus consumer-coordination helpers. `define` produces a typed spec...
- [ToolEnv](https://docs.kleisli.io/metaBuilder/ornaments/toolEnv): toolEnv ornament: typed tool-environment vocabulary for builder consumers. The spec carries only a typed `tools : [ToolSpec]` list; eliminators derive `toolI...
- [Testing](https://docs.kleisli.io/metaBuilder/ornaments/testing): TestingBuilder ornament over ProjectBuilder: typed test-suite declarations. `testCase` / `testSuite` smart constructors validate at the boundary; `selectCase...
- [Vendoring](https://docs.kleisli.io/metaBuilder/ornaments/vendoring): VendoringBuilder ornament over ProjectBuilder: a typed contract describing the structural fields a vendored package must declare. The contract itself is a ty...
- [Code-gen](https://docs.kleisli.io/metaBuilder/ornaments/code-gen): CodeGenBuilder ornament over BuilderSpec, with a `codeGen` smart constructor that produces typed multi-language code-generation specs.
- [Idl](https://docs.kleisli.io/metaBuilder/ornaments/idl): IdlBuilder ornament over CodeGenBuilder, with a `fromProtobuf` smart constructor that produces typed multi-language protobuf code-generation specs.
- [Capabilities](https://docs.kleisli.io/metaBuilder/ornaments/capabilities): capabilities ornament: typed capability vocabulary over the runtime.* effect algebra. Built-in `lifecycle`/`crud`/`streaming` categories, smart constructors ...
- [Protocol](https://docs.kleisli.io/metaBuilder/ornaments/protocol): protocol ornament: typed protocol vocabulary over the runtime.* effect algebra. Built-in protocols (rpc/json-rpc/dbus/grpc) as typed `ProtocolSpec` values, p...
- [Service](https://docs.kleisli.io/metaBuilder/ornaments/service): service ornament: typed service definition over the runtime.* effect algebra. `define` wraps the ServiceSpec smart constructor (with eager capability/protoco...
- [ReplServer](https://docs.kleisli.io/metaBuilder/ornaments/replServer): replServer ornament: typed REPL-server specification over the locked runtime.* algebra. `define` smart-ctor produces a `REPLServerSpec` with eager structural...
- [Sandbox](https://docs.kleisli.io/metaBuilder/ornaments/sandbox): sandbox ornament: typed sandbox profile over the bwrap/Landlock/seccomp/systemd backends. Four eliminators (toBwrap/toLandlock/toSeccomp/toSystemd) consume t...
- [Transform](https://docs.kleisli.io/metaBuilder/ornaments/transform): metaBuilder transform ornament: typed smart constructor over BuilderSpec for the multi-tool sequential transform-output pipeline shape. Each step becomes a r...
- [Oci-image](https://docs.kleisli.io/metaBuilder/ornaments/oci-image): OciImageBuilder ornament over BuilderSpec, with an `ociImage` smart constructor that compiles image fields into a named-step OCI layout assembly program.

#### Library Helpers

- [Tool-env](https://docs.kleisli.io/metaBuilder/lib/tool-env): metaBuilder tool-env lib: typed bundle of `ToolSpec` records describing a tool environment. The typed list is the API — shell-script glue (binPath strings,...
- [Toolchain](https://docs.kleisli.io/metaBuilder/lib/toolchain): metaBuilder toolchain lib: typed hint-based implementation selection and toolchain matrix construction.
- [Passthru](https://docs.kleisli.io/metaBuilder/lib/passthru): metaBuilder passthru lib: typed language-tagged package metadata. PassthruSpec carries `langName`, `baseName`, `baseDeps`, and an open `extensions` attrset; ...
- [Bundled](https://docs.kleisli.io/metaBuilder/lib/bundled): metaBuilder bundled lib: typed descriptor for system-bundled packages provided by a language implementation. The constructor tag itself is the bundled-vs-cus...
- [Dashboard](https://docs.kleisli.io/metaBuilder/lib/dashboard): metaBuilder dashboard lib: typed lock-metrics and workspace-summary interfaces for cross-language build dashboards.
- [ContentAddress](https://docs.kleisli.io/metaBuilder/lib/contentAddress): Opt a reproducible derivation into floating content-addressing (drv -> drv). Output path keyed by realised content; enables early-cutoff and cross-machine re...

### Additional pages (including unstable internal surfaces)

- [Examples](https://docs.kleisli.io/metaBuilder/examples/index): Runnable example builders that demonstrate metaBuilder internalized programs.
- [Manual](https://docs.kleisli.io/metaBuilder/manual/index): Practical guidance for writing and using metaBuilder builders as typed descriptions with reusable program views.
- [Theory](https://docs.kleisli.io/metaBuilder/theory/index): Mathematical framing for builders as descriptions, internalized programs, ornaments, interpretations, and runtime structure.

## nix-effects

Pure Nix effects, typed validation, verified boundaries, and description-backed DSLs.

### Manual

#### Guide

- [Introduction](https://docs.kleisli.io/nix-effects/guide/introduction): nix-effects is a typed, description-backed programming substrate for pure Nix that runs every check at nix eval time before anything builds.
- [Getting Started](https://docs.kleisli.io/nix-effects/guide/getting-started): Install nix-effects as a flake input or direct import, define a first type with fx.types, and run a computation through fx.run with a handler.
- [Effects and Handlers](https://docs.kleisli.io/nix-effects/guide/effects-and-handlers): Algebraic effects (send/bind/pure plus handlers) separate program intent from execution policy; the substrate underlies fx.types, diagnostics, and the checker.
- [Typed Validation](https://docs.kleisli.io/nix-effects/guide/typed-validation): fx.types wraps Nix value predicates with kernel-backed type information; refinements layer guard predicates over structural checks via fx.refine.
- [Generated Datatypes](https://docs.kleisli.io/nix-effects/guide/generated-datatypes): H.datatype generates a Nix record whose constructors, type, and description are reusable by the checker, generic walkers, schemas, and ornaments.
- [Generic Programming](https://docs.kleisli.io/nix-effects/guide/generic-programming): fx.types.generic consumes the levitated Desc of generated datatypes so checker, derive, and schema agree by sharing one metadata tree per type.
- [Ornaments and Description-Backed Data](https://docs.kleisli.io/nix-effects/guide/ornaments): Ornaments refine one generated datatype into another while preserving a forgetful map back, so enriched values stay usable wherever the base value fit.
- [Proof Guide](https://docs.kleisli.io/nix-effects/guide/proof-guide): Build proofs in nix-effects from Refl through the J eliminator to verified extraction of plain Nix functions from kernel-checked HOAS terms via NbE.
- [Sugar](https://docs.kleisli.io/nix-effects/guide/sugar): fx.sugar adds opt-in syntax (do, /, steps, letM, with, wrap) over the effect substrate; the kernel never imports it and removing it changes nothing.

#### Concepts

- [Theory](https://docs.kleisli.io/nix-effects/concepts/theory): Papers behind nix-effects: Plotkin-Pretnar handlers, the freer monad, FTCQueue, Martin-Lof type theory, normalization by evaluation, and levitated descriptions.

#### Internals

- [Trampoline](https://docs.kleisli.io/nix-effects/internals/trampoline): builtins.genericClosure trampolines the freer-monad interpreter to O(1) stack depth in Nix, which lacks both iteration primitives and tail-call elimination.
- [Kernel Architecture](https://docs.kleisli.io/nix-effects/internals/kernel-architecture): The type-checking kernel layers a TCB (eval/quote/conv) under the bidirectional check/infer pair; errors are sent as typeError effects, not thrown.
- [Kernel Formal Specification](https://docs.kleisli.io/nix-effects/internals/kernel-spec): Formal contract for the type-checking kernel: trust layers, typing rules, compute and conversion rules, and invariants the implementation must maintain.

### Examples

#### Overview


#### Proofs

- [Proof Basics](https://docs.kleisli.io/nix-effects/proof-examples/proofBasics): Computational proof examples checked by the HOAS kernel and exposed as ordinary Nix values.
- [Equality Proofs](https://docs.kleisli.io/nix-effects/proof-examples/equalityProofs): Derive reusable equality combinators from the J eliminator and check them through the kernel.
- [Verified Functions](https://docs.kleisli.io/nix-effects/proof-examples/verifiedFunctions): Kernel-checked HOAS programs extracted into plain Nix functions.

#### Effects and Validation

- [Handler-Swap Validation](https://docs.kleisli.io/nix-effects/effect-examples/handlerSwapValidation): Run one validation computation with collecting, logging, and strict handlers.

#### Surface Languages

- [Surface STLC](https://docs.kleisli.io/nix-effects/surface-examples/stlc): Surface-language walkthroughs for a simply typed lambda calculus.
- [STLC Core Surface](https://docs.kleisli.io/nix-effects/surface-examples/stlc/core): A simply typed lambda-calculus surface over the HOAS kernel.
- [STLC Sums and Products](https://docs.kleisli.io/nix-effects/surface-examples/stlc/sumsProducts): Extend the STLC surface with product and sum syntax while reusing the existing HOAS kernel.
- [STLC Recursive Lists](https://docs.kleisli.io/nix-effects/surface-examples/stlc/recursiveLists): List syntax and folds over description-backed recursive data.
- [STLC Refinements and Diagnostics](https://docs.kleisli.io/nix-effects/surface-examples/stlc/refinementsDiagnostics): Add refinement syntax to the STLC surface while preserving source-level diagnostic classes.

#### Applications

- [Category Theory](https://docs.kleisli.io/nix-effects/application-examples/categoryTheory): Kernel-checked arithmetic, algebra, functors, and Yoneda-style constructions.
- [Expression Interpreter](https://docs.kleisli.io/nix-effects/application-examples/interp): A small expression language interpreted with lookup, scoped environment, and failure effects.
- [Build Simulator](https://docs.kleisli.io/nix-effects/application-examples/buildSim): A dependency-graph evaluator with cache, configuration, logging, and failure effects.

### API Reference

#### Core API

- [Kernel](https://docs.kleisli.io/nix-effects/core-api/kernel): Freer monad kernel: `send`/`bind`/`map`/`seq`/`pipe`/`kleisli` over the `Computation` ADT with FTCQueue continuations for O(1) bind.
- [Comp](https://docs.kleisli.io/nix-effects/core-api/comp): Computation ADT: `pure`/`impure` constructors plus `match`/`isComp`/`isPure` eliminators — the freer-monad value representation other modules build on.
- [Binds](https://docs.kleisli.io/nix-effects/core-api/binds): Idiomatic Nix bind helpers: `bindAttrs`/`bindComp`/`bindFn` lift attrset/function shapes into effect chains; `optionalArg` marks attrs as handler-conditional.
- [Trampoline](https://docs.kleisli.io/nix-effects/core-api/trampoline): Trampolined interpreter: `run`/`handle`/`rotate` drive computations via `builtins.genericClosure` at O(1) stack depth and Kyo-style rotation.
- [Queue](https://docs.kleisli.io/nix-effects/core-api/queue): FTCQueue (catenable queue, Kiselyov & Ishii 2015): `leaf`/`node`/`singleton`/`snoc`/`append`/`viewl`/`qApp` — O(1) bind on linearly nested computation chains.
- [Adapt](https://docs.kleisli.io/nix-effects/core-api/adapt): Handler context transformation: `adapt`/`adaptHandlers` reposition handlers onto larger state via lenses — contravariant on context, covariant on continuat...
- [Pipeline](https://docs.kleisli.io/nix-effects/core-api/pipeline): Typed pipeline: `mkStage`/`compose`/`run` build composable stages over reader/error/acc handlers, collecting errors, warnings, and type errors.
- [State](https://docs.kleisli.io/nix-effects/core-api/state): fx.state: deepSeq-safe carrier for arbitrary values in handler state — `mkThunk`/`forceThunk` shield Nix closures from the trampoline per-step deepSeq.
- [Thunk](https://docs.kleisli.io/nix-effects/core-api/state/thunk): Thunk: deepSeq-safe carrier for transporting values through trampoline-threaded handler state via a closure that hides the value from `builtins.deepSeq`.
- [Sugar](https://docs.kleisli.io/nix-effects/core-api/sugar): fx.sugar: opt-in syntax layer for the effect substrate — do, /, steps, letM, with, wrap — that compiles down to plain bind/pure/send.
- [Build](https://docs.kleisli.io/nix-effects/core-api/build): fx.build: eval-time build pipeline — `plan` validates BuildStep records via fx.pipeline, `materialize` lowers a plan to a runCommand derivation.
- [Types](https://docs.kleisli.io/nix-effects/core-api/build/types): Build types: `BuildStep`/`BuildPlan` open-record schemas that validate build pipelines at eval time before materialisation into derivations.
- [Experimental](https://docs.kleisli.io/nix-effects/core-api/experimental): fx.experimental: unstable surfaces under active development — currently the description-side `desc-interp` substrate where FreeFx lives as a μ-tree.
- [Desc-interp](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp): fx.experimental.desc-interp: FreeFx as a μ-tree on HOAS descriptions — `kernel` provides pure/send/bind, `trampoline` runs programs via genericClosure.
- [Compose](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/compose): fx.experimental.desc-interp.compose: universal handler-result type UniRet and its smart constructors. Every kernel-resident handler can be re-shaped into a U...
- [Compose-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/compose-laws): fx.experimental.desc-interp.compose-laws: kernel-checked one-shot meta-theorem for composeHandlers. Two clauses (inl/inr); both discharge by H.refl.
- [Composed-shortcut](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/composed-shortcut): fx.experimental.desc-interp.composed-shortcut: closes per-effect UShortHand shortcuts under `composeHandlers`. `composedHandlerShortcut` mirrors `eval (compo...
- [Composed-shortcut-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/composed-shortcut-laws): fx.experimental.desc-interp.composed-shortcut-laws: six H.refl lemmas — state's three canonical ops on inl and error's three strategies on inr — anchorin...
- [Desc](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/desc): fx.experimental.desc-interp.desc: freer monad encoded as a levitated Desc (freeFx = pure + impure plus continuation queue); the substrate descInterp runs.
- [Descind-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/descind-laws): fx.experimental.desc-interp.descind-laws: kernel-level laws derived via `descInd kontQueueApp` at the indexed slice. Hosts qAppKernel (kernel-resident transp...
- [Effects](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects): fx.experimental.desc-interp.effects: error, state, and typecheck effects over the description-side kernel — `error` raises, `EffState` is kernel-resident w...
- [Error](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/error): error effect over descInterp's FreeFx kernel — EffError datatype + three kernel-term handlers (strict/collecting/result) with paired dispatch interpreters.
- [Error-shortcut-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/error-shortcut-laws): fx.experimental.desc-interp.effects.error-shortcut-laws: kernel-checked one-shot lemmas for each `handle_*` on the canonical EffError raise. Each lemma disch...
- [Error-uniform-shortcut-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/error-uniform-shortcut-laws): fx.experimental.desc-interp.effects.error-uniform-shortcut-laws: kernel-checked H.refl lemmas certifying that each `uniformOf_*` on the canonical EffError ra...
- [State](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/state): state effect over descInterp's FreeFx kernel — EffState kernel datatype + kernel-term handle_State; smart constructors + `{ handler; dispatch }` bridge rec...
- [State-shortcut-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/state-shortcut-laws): fx.experimental.desc-interp.effects.state-shortcut-laws: kernel-checked one-shot lemmas for handle_State on each canonical EffState op (get/put/modify). Each...
- [Typecheck](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/typecheck): typecheck-policy handlers over descInterp's FreeFx kernel — EffTypeCheck datatype (one `report(reason, path, carrier, passed)` op) + six kernel-term handle...
- [Typecheck-shortcut-laws](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/effects/typecheck-shortcut-laws): fx.experimental.desc-interp.effects.typecheck-shortcut-laws: kernel-checked one-shot lemmas certifying each typecheck handler on the canonical `report` op re...
- [Extract](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/extract): fx.experimental.desc-interp.extract: partial-evaluation emitter for kernel-resident handler shortcuts. ResidualForm algebra + `extract : RF → Val` mirrorin...
- [Kernel](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/kernel): fx.experimental.desc-interp.kernel: pure/send/bind constructors producing FreeFx Desc values directly as `μ freeFxApp` data, not Nix-host computations.
- [Trampoline](https://docs.kleisli.io/nix-effects/core-api/experimental/desc-interp/trampoline): fx.experimental.desc-interp.trampoline: qApp/run/handle interpreters trampolining FreeFx Desc values via genericClosure for O(1) stack depth on long chains.

#### Diagnostics

- [Positions](https://docs.kleisli.io/nix-effects/diag/positions): fx.diag.positions: shared diagnostic alphabet of structural sub-locations (DArgSort, DPlusL, PiDom, …) carrying tag, segment, intent, and rule annotation.
- [Error](https://docs.kleisli.io/nix-effects/diag/error): fx.diag.error: diagnostic Error ADT — Layer (Kernel/Generic/Contract), layer-discriminated Detail, msg, hint, and children tree carrying the blame path.
- [Hints](https://docs.kleisli.io/nix-effects/diag/hints): fx.diag.hints: closed registry mapping blame-path-suffix keys to Hint records; `resolve` walks an Error's chain inward and returns the longest-suffix match.
- [Pretty](https://docs.kleisli.io/nix-effects/diag/pretty): fx.diag.pretty: pretty-print diagnostic Errors — `pathSegments`/`pathString`/`oneLine`/`multiLine` walkers, stack-safe via genericClosure past 500 frames.

#### Effects

- [State](https://docs.kleisli.io/nix-effects/effects/state): state effect: mutable state threaded by the handler; get/put/modify with update/gets sugar and a standard handler.
- [Reader](https://docs.kleisli.io/nix-effects/effects/reader): reader effect: read-only environment threaded as immutable state; ask/asks/local with a standard handler. Read-only restriction of state.
- [Writer](https://docs.kleisli.io/nix-effects/effects/writer): writer effect: append-only output via tell/tellAll with a list-collecting handler. Append-only restriction of state.
- [Acc](https://docs.kleisli.io/nix-effects/effects/acc): acc effect: incremental list building via emit/emitAll/collect with a default handler that appends to a list state.
- [Error](https://docs.kleisli.io/nix-effects/effects/error): error effect: raise/raiseWith with three handler strategies — strict (throw), collecting (accumulate list), and result (tagged abort).
- [Conditions](https://docs.kleisli.io/nix-effects/effects/conditions): conditions effect: Common-Lisp-style signal/warn with restart-based recovery; handler IS the algebra choosing among offered restarts.
- [Choice](https://docs.kleisli.io/nix-effects/effects/choice): choice effect: non-deterministic computation via choose/fail/guard with a listAll handler that explores every branch (list-monad semantics).
- [Scope](https://docs.kleisli.io/nix-effects/effects/scope): scope effect: computation-scoped handlers via Kyo-style effect rotation; provide/val/stateful/run/runWith plus handlersFromAttrs sugar.
- [Linear](https://docs.kleisli.io/nix-effects/effects/linear): linear effect: graded resource discipline (linear, affine, exact n, unlimited) via acquire/consume/release with a finalizer enforcing usage bounds.
- [Typecheck](https://docs.kleisli.io/nix-effects/effects/typecheck): typecheck effect handlers: strict / collecting / logging / firstN / summarize / pretty under `policy.*`; bridge between the type system and effects.
- [HasHandler](https://docs.kleisli.io/nix-effects/effects/hasHandler): hasHandler: ask the runtime whether a handler with the given effect name exists in the surrounding scope; impure query.

#### Types

- [Foundation](https://docs.kleisli.io/nix-effects/types/foundation): Type system foundation: `mkType`/`check`/`validate`/`make`/`refine` build types from kernel HOAS representations and the guard/effect machinery underneath.
- [Primitives](https://docs.kleisli.io/nix-effects/types/primitives): Primitive types: String/Int/Bool/Float/Attrs/Path/Derivation/Function/Null/Unit/Any — universe-0 atomic types corresponding to Nix's value categories.
- [Constructors](https://docs.kleisli.io/nix-effects/types/constructors): Type constructors: Record/RecordOpen/ListOf/Maybe/Either/Variant — higher-kinded builders composing simpler types with per-component blame.
- [Refinement](https://docs.kleisli.io/nix-effects/types/refinement): Refinement types: `refined` plus `allOf`/`anyOf`/`negate`, raw built-in predicates `positive`/`nonNegative`/`inRange`/`nonEmpty`/`matching`, and the kernel-i...
- [Dependent](https://docs.kleisli.io/nix-effects/types/dependent): fx.types.dependent: dependent contracts Pi (Π), Sigma (Σ), Certified, Vector, DepRecord — higher-order contracts checked incrementally at each applicatio...
- [Linear](https://docs.kleisli.io/nix-effects/types/linear): Linear type constructors: `Linear`/`Affine`/`Graded` — pure structural guards for capability tokens; usage enforcement lives in the linear effect handler.
- [Universe](https://docs.kleisli.io/nix-effects/types/universe): Universe hierarchy: `typeAt n` produces `Type_n` in a non-cumulative Tarski tower; `lift`/`liftTo` coerce across levels; `Type_0`–`Type_4` are predefined; ...

#### Streams

- [Core](https://docs.kleisli.io/nix-effects/streams/core): Stream primitives: `done`/`more`/`fromList`/`iterate`/`range`/`replicate` — constructors for lazy `Step`-tagged streams composed via bind.
- [Transform](https://docs.kleisli.io/nix-effects/streams/transform): Stream transformations: `map`/`filter` plus `scanl`/`flatMap` — pure rewrites that produce new streams from existing ones.
- [Limit](https://docs.kleisli.io/nix-effects/streams/limit): Stream limiting: `take`/`takeWhile`/`drop` — bound stream length by count or predicate.
- [Combine](https://docs.kleisli.io/nix-effects/streams/combine): Stream combination: `concat`/`interleave`/`zip`/`zipWith` — merge two streams sequentially, alternately, or positionally.
- [Reduce](https://docs.kleisli.io/nix-effects/streams/reduce): Stream reduction: `fold`/`toList`/`length`/`sum`/`signal`/`signalOn`/`any`/`all` — terminal operations that consume a stream into a single computation.

#### Type Checker

- [Term](https://docs.kleisli.io/nix-effects/type-checker/term): fx.tc.term: kernel term constructors (Pi, Sigma, U, Id, J, datatype/desc nodes) de-Bruijn indexed; each carries `tag` distinct from value-domain `_tag`.
- [Value](https://docs.kleisli.io/nix-effects/type-checker/value): fx.tc.value: semantic domain produced by evaluation; values use de Bruijn LEVELS (counting outward) so substitution under binders stays unproblematic.
- [Quote](https://docs.kleisli.io/nix-effects/type-checker/quote): fx.tc.quote: TCB read-back from values to terms, translating de Bruijn levels back to indices; pure, no type information, no effects.
- [Conv](https://docs.kleisli.io/nix-effects/type-checker/conv): fx.tc.conv: structural conversion check on de Bruijn level values; pure TCB component asking whether two values are definitionally equal at a given depth.
- [Eval](https://docs.kleisli.io/nix-effects/type-checker/eval): fx.tc.eval: pure kernel evaluator for `eval`/`evalF`/`instantiate` plus elimination helpers; zero effect-system imports, part of the TCB.
- [_internal](https://docs.kleisli.io/nix-effects/type-checker/eval/_internal): fx.tc.eval._internal: cross-part evaluator helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.
- [Dispatch](https://docs.kleisli.io/nix-effects/type-checker/eval/dispatch): fx.tc.eval.dispatch: full kernel evaluator self-fixpoint. Consumed by overlay constructions (notably `tc/elaborate/eval-overlay.nix`) that need to build a me...
- [Check](https://docs.kleisli.io/nix-effects/type-checker/check): fx.tc.check: bidirectional type checker with check/infer/checkType/checkTypeLevel, non-cumulative universes, and trampolined succ/cons chains.
- [Diag](https://docs.kleisli.io/nix-effects/type-checker/check/diag): fx.tc.check.diag: outside-the-trust-boundary diagnostic shell that routes kernel `check`/`infer` results, attaches hints, and formats failures for editors.
- [_internal](https://docs.kleisli.io/nix-effects/type-checker/check/_internal): fx.tc.check._internal: cross-part checker helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.
- [Elaborate](https://docs.kleisli.io/nix-effects/type-checker/elaborate): fx.tc.elaborate: bridge between `fx.types` and the kernel — `elaborateType`/`elaborateValue`/`extract`/`decide` translate values to kernel terms and back.
- [Meta](https://docs.kleisli.io/nix-effects/type-checker/elaborate/meta): fx.tc.elaborate.meta: meta-aware overlay — `VMeta`, overlay check/infer, overlay eliminators, quote, `elabConv`, five scoped meta-effects (force/getMetas/a...
- [_internal](https://docs.kleisli.io/nix-effects/type-checker/elaborate/_internal): fx.tc.elaborate._internal: cross-part elaboration helpers reachable from sibling parts via the self-fixpoint; not part of the stable consumer surface.
- [Hoas](https://docs.kleisli.io/nix-effects/type-checker/hoas): fx.tc.hoas: HOAS surface combinators for kernel terms — types, binders, descriptions, datatypes, ornaments, and the lowering pass that compiles to de Bruij...
- [_internal](https://docs.kleisli.io/nix-effects/type-checker/hoas/_internal): Unstable internal surface — boot-sum/boot-eq helpers, kernel-Tm encoders, and indexed-variant scaffolding; prefer SumDT/EqDT-generated forms in user code.
- [_encoders](https://docs.kleisli.io/nix-effects/type-checker/hoas/_internal/_encoders): Kernel-Tm and Val-level encoders for surface description combinators; consumed by `tc/eval` (descDescVal) and `tc/generic` (encodeDescXTm pre-evaluations).
- [_forced](https://docs.kleisli.io/nix-effects/type-checker/hoas/_internal/_forced): Forced-argument analysis helpers for datatype constructors; consumed by datatype elaboration and tests that inspect recoverable constructor fields.
- [_indexed](https://docs.kleisli.io/nix-effects/type-checker/hoas/_internal/_indexed): Indexed/equality-aligned combinators (`muI`, `piI`, `recI`, `plusI`, `inrAt`, `fieldAt`) consumed by ornament construction and indexed-datatype test fixtures.
- [Surface](https://docs.kleisli.io/nix-effects/type-checker/surface): fx.tc.surface: additive surface-language elaboration framework over HOAS.
- [Registry](https://docs.kleisli.io/nix-effects/type-checker/surface/registry): Surface elaborator registry operations. empty Empty surface elaboration registry. copyexpandRegistry emptyRegistry...
- [Generic](https://docs.kleisli.io/nix-effects/type-checker/generic): fx.tc.generic: datatype-generic reflection over levitated descriptions — desc/datatype/value/derive helpers plus the algebraic/functional ornaments surface.
- [Desc](https://docs.kleisli.io/nix-effects/type-checker/generic/desc): desc: views and folds over levitated descriptions — `descView` peels one layer, `foldDesc` recurses, `mapDesc` rewrites, predicates split by constructor.
- [Datatype](https://docs.kleisli.io/nix-effects/type-checker/generic/datatype): datatype: normalise + lookup over `_dtypeMeta` — extract canonical constructor / field lists, resolve dependent field types, instantiate polymorphic parame...
- [Value](https://docs.kleisli.io/nix-effects/type-checker/generic/value): value: bidirectional views over generated datatypes — `view`/`review` swap HOAS and Nix constructor records; `fold` and `mapChildren` operate generically.
- [Derive](https://docs.kleisli.io/nix-effects/type-checker/generic/derive): derive: structured artifacts from datatype metadata — type descriptors, JSON-Schema, docs scaffolds, fold scaffolds, and node-and-edge dependency graphs.
- [Check](https://docs.kleisli.io/nix-effects/type-checker/generic/check): check: canonical typed walker over the HOAS algebra — one fold at two carriers (unit for validation, HOAS for elaboration), plus refinement-guard composition.
- [CheckD](https://docs.kleisli.io/nix-effects/type-checker/generic/checkD): checkD: generic bidirectional checker for Desc payloads — validates terms against `interpD level I D X i` by walking the description.
- [Ornaments](https://docs.kleisli.io/nix-effects/type-checker/generic/ornaments): ornaments: algebraic + functional ornament constructions over generated datatypes — spec validation, fold/producer/transform lifting, and forgetful maps.
- [Verified](https://docs.kleisli.io/nix-effects/type-checker/verified): fx.tc.verified: high-level combinators for writing kernel-checked implementations; build a program, call `.verify` to type-check it against the kernel.
- [Kernel](https://docs.kleisli.io/nix-effects/type-checker/kernel): fx.tc.kernel: kernel-internalized `validate` via the flat predicate-stack KType / El family (base-and-predicate factoring).

#### Diagnostic Hints

- [DArgSort::universe-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/dargsort-universe-mismatch): DArgSort::universe-mismatch — the sort position of `arg` must live in U(0); descriptions only carry small types.
- [DPiSort::universe-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/dpisort-universe-mismatch): DPiSort::universe-mismatch — the sort position of `pi` must live in U(0); `descPi` takes a small domain.
- [LevelMaxLhs::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/levelmaxlhs-type-mismatch): LevelMaxLhs::type-mismatch — the left operand of `max` must be a Level.
- [LevelMaxRhs::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/levelmaxrhs-type-mismatch): LevelMaxRhs::type-mismatch — the right operand of `max` must be a Level.
- [LevelSucPred::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/levelsucpred-type-mismatch): LevelSucPred::type-mismatch — the predecessor of `suc` must be a Level.
- [ULevel::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/ulevel-type-mismatch): ULevel::type-mismatch — the level argument of `U` must be a Level.
- [AnnType::not-a-type](https://docs.kleisli.io/nix-effects/diag-hints/anntype-not-a-type): AnnType::not-a-type — the annotation position must be a type (live in some U(k)), not a term.
- [JType::not-a-type](https://docs.kleisli.io/nix-effects/diag-hints/jtype-not-a-type): JType::not-a-type — the type parameter of `J` must be a type (live in some U(k)), not a term.
- [Motive.PiDom::not-a-type](https://docs.kleisli.io/nix-effects/diag-hints/motive-pidom-not-a-type): Motive.PiDom::not-a-type — the motive's domain must be a type (live in some U(k)).
- [Motive::not-a-type](https://docs.kleisli.io/nix-effects/diag-hints/motive-not-a-type): Motive::not-a-type — an eliminator's motive must return a type (live in some U(k)).
- [PiCod::not-a-type](https://docs.kleisli.io/nix-effects/diag-hints/picod-not-a-type): PiCod::not-a-type — the codomain family of Π must return a type for each argument, not an ordinary value.
- [PiDom::not-a-type](https://docs.kleisli.io/nix-effects/diag-hints/pidom-not-a-type): PiDom::not-a-type — the domain of Π must be a type (live in some U(k)), not a term or value.
- [DArgBody::not-a-desc](https://docs.kleisli.io/nix-effects/diag-hints/dargbody-not-a-desc): DArgBody::not-a-desc — the body of `arg` must produce a description (Desc I), not an ordinary value.
- [DPiBody::not-a-desc](https://docs.kleisli.io/nix-effects/diag-hints/dpibody-not-a-desc): DPiBody::not-a-desc — the body of `pi` must produce a description for each input, not a plain term.
- [DPlusL::not-a-desc](https://docs.kleisli.io/nix-effects/diag-hints/dplusl-not-a-desc): DPlusL::not-a-desc — the left summand of `plus` must be a description (Desc I).
- [DPlusR::not-a-desc](https://docs.kleisli.io/nix-effects/diag-hints/dplusr-not-a-desc): DPlusR::not-a-desc — the right summand of `plus` must be a description at the same index type as the left summand.
- [DRecTail::not-a-desc](https://docs.kleisli.io/nix-effects/diag-hints/drectail-not-a-desc): DRecTail::not-a-desc — the tail position of `rec` must itself be a description, not an ordinary term.
- [MuDesc::not-a-desc](https://docs.kleisli.io/nix-effects/diag-hints/mudesc-not-a-desc): MuDesc::not-a-desc — the description argument of μ must be a Desc I term, not an ordinary value.
- [AppHead::not-a-function](https://docs.kleisli.io/nix-effects/diag-hints/apphead-not-a-function): AppHead::not-a-function — the head of an application must have a function type (Pi).
- [DPiFn::not-a-function](https://docs.kleisli.io/nix-effects/diag-hints/dpifn-not-a-function): DPiFn::not-a-function — the index selector `f` of `pi` must be a function `S -> I`.
- [Motive::not-a-function](https://docs.kleisli.io/nix-effects/diag-hints/motive-not-a-function): Motive::not-a-function — the motive must be a function from the scrutinee's type into a type, not a bare type or value.
- [OpaqueType::not-a-function](https://docs.kleisli.io/nix-effects/diag-hints/opaquetype-not-a-function): OpaqueType::not-a-function — the annotation on an opaque lambda must be a Pi type.
- [DPiFn::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/dpifn-type-mismatch): DPiFn::type-mismatch — the index selector's domain must match the declared sort `S`.
- [DRecIndex::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/drecindex-type-mismatch): DRecIndex::type-mismatch — the index position of `rec` must match the Desc's declared index type.
- [DRetIndex::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/dretindex-type-mismatch): DRetIndex::type-mismatch — the index position of `ret` must match the Desc's declared index type.
- [MuIndex::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/muindex-type-mismatch): MuIndex::type-mismatch — the index passed to `con` must have the description's index type.
- [MuPayload::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/mupayload-type-mismatch): MuPayload::type-mismatch — the payload of `con` must inhabit the description's interpretation at the given index.
- [Elem::inhabitation-failed](https://docs.kleisli.io/nix-effects/diag-hints/elem-inhabitation-failed): Elem::inhabitation-failed — the element does not inhabit the list's element type.
- [Field::inhabitation-failed](https://docs.kleisli.io/nix-effects/diag-hints/field-inhabitation-failed): Field::inhabitation-failed — the field's value does not inhabit the declared field type.
- [SigmaFst::inhabitation-failed](https://docs.kleisli.io/nix-effects/diag-hints/sigmafst-inhabitation-failed): SigmaFst::inhabitation-failed — the first component does not inhabit the declared `fst` type.
- [SigmaSnd::inhabitation-failed](https://docs.kleisli.io/nix-effects/diag-hints/sigmasnd-inhabitation-failed): SigmaSnd::inhabitation-failed — the second component does not inhabit the dependent `snd` type.
- [Tag::inhabitation-failed](https://docs.kleisli.io/nix-effects/diag-hints/tag-inhabitation-failed): Tag::inhabitation-failed — the variant's payload does not inhabit the branch type.
- [Elem::refinement-failed](https://docs.kleisli.io/nix-effects/diag-hints/elem-refinement-failed): Elem::refinement-failed — the element violates the element type's refinement predicate.
- [Field::refinement-failed](https://docs.kleisli.io/nix-effects/diag-hints/field-refinement-failed): Field::refinement-failed — the field's value violates the field type's refinement predicate.
- [SigmaFst::refinement-failed](https://docs.kleisli.io/nix-effects/diag-hints/sigmafst-refinement-failed): SigmaFst::refinement-failed — the first component violates the `fst` type's refinement predicate.
- [SigmaSnd::refinement-failed](https://docs.kleisli.io/nix-effects/diag-hints/sigmasnd-refinement-failed): SigmaSnd::refinement-failed — the second component violates the `snd` type's refinement predicate.
- [Tag::refinement-failed](https://docs.kleisli.io/nix-effects/diag-hints/tag-refinement-failed): Tag::refinement-failed — the variant's payload violates the branch type's refinement predicate.
- [Case::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/case-type-mismatch): Case::type-mismatch — this case-body's inferred type does not match the type the eliminator's motive requires.
- [Scrut::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/scrut-type-mismatch): Scrut::type-mismatch — the scrutinee's type must match the eliminator's expected shape.
- [AnnTerm::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/annterm-type-mismatch): AnnTerm::type-mismatch — the annotated term does not match its declared type.
- [AppArg::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/apparg-type-mismatch): AppArg::type-mismatch — the argument does not match the function's domain.
- [JType::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/jtype-type-mismatch): JType::type-mismatch — the type parameter of `J` must match the type of its two endpoints.
- [OpaqueType::type-mismatch](https://docs.kleisli.io/nix-effects/diag-hints/opaquetype-type-mismatch): OpaqueType::type-mismatch — the opaque lambda's declared domain does not match the expected domain.
- [::unhandled-boot-inl](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-boot-inl): ::unhandled-boot-inl — the left injection `inl x` has no inference rule — the sum type's right summand is not determined by the syntax of `x` alone.
- [::unhandled-boot-inr](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-boot-inr): ::unhandled-boot-inr — the right injection `inr y` has no inference rule — the sum type's left summand is not determined by the syntax of `y` alone.
- [::unhandled-boot-refl](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-boot-refl): ::unhandled-boot-refl — `refl` has no inference rule — the type of the equated endpoint is not determined by its syntax.
- [::unhandled-lam](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-lam): ::unhandled-lam — this lambda has no inference rule — its domain and codomain types are not determined by its syntax.
- [::unhandled-other](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-other): ::unhandled-other — this intro form has no inference rule — its type is not determined by its syntax alone.
- [::unhandled-pair](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-pair): ::unhandled-pair — this pair has no inference rule — its component types are not determined by its syntax.
- [::unhandled-tt](https://docs.kleisli.io/nix-effects/diag-hints/unhandled-tt): ::unhandled-tt — the unit value `tt` has no inference rule — there is exactly one type it can inhabit.

### Additional pages (including unstable internal surfaces)

- [Applications](https://docs.kleisli.io/nix-effects/application-examples/index): Complete example programs that double as benchmark workloads.
- [Concepts](https://docs.kleisli.io/nix-effects/concepts/index): Background concepts behind nix-effects: handlers, freer monads, queues, normalization by evaluation, and description-backed data.
- [Diagnostic Hints](https://docs.kleisli.io/nix-effects/diag-hints/index): Stable diagnostic Hint keys for checker and validation failures, with focused pages for each emitted key.
- [Effects and Validation](https://docs.kleisli.io/nix-effects/effect-examples/index): Effect-handler walkthroughs that show one computation running under multiple validation policies.
- [Examples](https://docs.kleisli.io/nix-effects/examples/index): Worked examples for proofs, effect-handler policy, small surface languages, and complete applications over HOAS.
- [Guide](https://docs.kleisli.io/nix-effects/guide/index): A practical path through nix-effects: start with imports and handlers, then move into typed validation, generated datatypes, ornaments, proofs, and syntax su...
- [Internals](https://docs.kleisli.io/nix-effects/internals/index): Implementation notes for the evaluator, type-checking kernel, trampoline, architecture, and formal kernel contract.
- [Proofs](https://docs.kleisli.io/nix-effects/proof-examples/index): Kernel-checked proof walkthroughs: computation, equality reasoning, and verified extraction.
- [Surface Languages](https://docs.kleisli.io/nix-effects/surface-examples/index): Small source-language walkthroughs built over HOAS, refinements, diagnostics, and generated data.

## Programmatic access (MCP)

An MCP (Model Context Protocol) server is available for programmatic access:

- Explainer: https://docs.kleisli.io/mcp
- Transport endpoint: https://docs.kleisli.io/mcp/transport
- Transport protocol: Streamable HTTP (POST/GET/DELETE per spec 2025-03-26)
- Tools: search_docs(query), get_page(project,section,page), list_projects()
- Resources: docs://kleisli/{project}/{section}/{page}

## Discovery affordances

Multiple discovery surfaces are exposed for AI agents and crawlers; they are redundant by design so that a client missing one channel still finds the others.

**HTML `<head>` tags** (visible to JS-rendering crawlers):

- `<link rel="alternate" type="text/markdown" href="/llms.txt">` — Mintlify-style index advertisement.
- `<meta name="ai-content-discovery" content="...">` — explicit directive enumerating all of the affordances below.

**HTTP response headers** (visible to non-JS fetchers; RFC 8288):

- `Link: </llms.txt>; rel="llms-txt"` on every response.
- `X-Llms-Txt: /llms.txt` on every response (custom fallback header for crawlers that don't parse Link).
- `Link: <{path}.md>; rel="llms-txt-page"` additionally on every doc-page response, pointing at the markdown alternate.

**Content negotiation** (`Accept` header):

- Send `Accept: text/markdown` on any project / section / page URL; the server returns `Content-Type: text/markdown; charset=utf-8` with the markdown source instead of HTML.

**Parallel `.md` routes** (suffix-based, no Accept header required):

- `https://docs.kleisli.io/{project}.md` — project-level markdown index (the per-project llms.txt).
- `https://docs.kleisli.io/{project}/{section}.md` — section overview as a bulleted markdown summary.
- `https://docs.kleisli.io/{project}/{section}/{page}.md` — the individual doc page's markdown source.

**Per-project & track-scoped indices**:

- `https://docs.kleisli.io/{project}/llms.txt` — one project's full index; `https://docs.kleisli.io/{project}/llms-full.txt` inlines its content.
- `https://docs.kleisli.io/{project}/{track}/llms.txt` — one reading track's index (e.g. learn, extend, reference), a smaller budget tier than the full per-project index.

**Full corpus**: `https://docs.kleisli.io/llms-full.txt` inlines every published page as one Markdown document.

**Crawler surfaces**: `https://docs.kleisli.io/sitemap.xml`, `https://docs.kleisli.io/robots.txt`, `https://docs.kleisli.io/changes.atom` (recently-updated feed), and `https://docs.kleisli.io/.well-known/mcp.json` (MCP server card, SEP-1649).