Kleisli.IO

kleisli.io kli blog docs

Theme

Navigation

Manual

Guide Introduction Getting Started Effects and Handlers Typed Validation Generated Datatypes Generic Programming Ornaments and Description-Backed Data Proof Guide Sugar

Concepts Theory

Internals Trampoline Systems Architecture Kernel Architecture Kernel Formal Specification

Examples

Proofs Proof Basics Equality Proofs Verified Functions

Effects and Validation Handler-Swap Validation

Surface Languages Surface STLC STLC Core Surface STLC Sums and Products STLC Recursive Lists STLC Refinements and Diagnostics

Applications Category Theory Expression Interpreter Build Simulator

API Reference

Core API Kernel Comp Binds Trampoline Queue Adapt Pipeline State Thunk Sugar Build Types Experimental Desc-interp Compose Compose-laws Composed-shortcut Composed-shortcut-laws Desc Descind-laws Effects Error Error-shortcut-laws Error-uniform-shortcut-laws State State-shortcut-laws Extract Kernel Trampoline

Diagnostics Positions Error Hints Pretty

Effects State Reader Writer Acc Error Conditions Choice Scope Linear Typecheck HasHandler

Types Foundation Primitives Constructors Refinement Dependent Linear Universe

Streams Core Transform Limit Combine Reduce

Type Checker Term Value Quote Conv Eval _internal Dispatch Check Diag _internal Elaborate Meta _internal Hoas _internal _encoders _forced _indexed Surface Registry Generic Desc Datatype Value Derive Check CheckD Ornaments Verified

Diagnostic Hints DArgSort::universe-mismatch DPiSort::universe-mismatch LevelMaxLhs::type-mismatch LevelMaxRhs::type-mismatch LevelSucPred::type-mismatch ULevel::type-mismatch AnnType::not-a-type JType::not-a-type Motive.PiDom::not-a-type Motive::not-a-type PiCod::not-a-type PiDom::not-a-type DArgBody::not-a-desc DPiBody::not-a-desc DPlusL::not-a-desc DPlusR::not-a-desc DRecTail::not-a-desc MuDesc::not-a-desc AppHead::not-a-function DPiFn::not-a-function Motive::not-a-function OpaqueType::not-a-function DPiFn::type-mismatch DRecIndex::type-mismatch DRetIndex::type-mismatch MuIndex::type-mismatch MuPayload::type-mismatch Elem::inhabitation-failed Field::inhabitation-failed SigmaFst::inhabitation-failed SigmaSnd::inhabitation-failed Tag::inhabitation-failed Elem::refinement-failed Field::refinement-failed SigmaFst::refinement-failed SigmaSnd::refinement-failed Tag::refinement-failed Case::type-mismatch Scrut::type-mismatch AnnTerm::type-mismatch AppArg::type-mismatch JType::type-mismatch OpaqueType::type-mismatch ::unhandled-boot-inl ::unhandled-boot-inr ::unhandled-boot-refl ::unhandled-lam ::unhandled-other ::unhandled-pair ::unhandled-tt

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

all pages, single document

Manual

Guide Introduction Getting Started Effects and Handlers Typed Validation Generated Datatypes Generic Programming Ornaments and Description-Backed Data Proof Guide Sugar

Concepts Theory

Internals Trampoline Systems Architecture Kernel Architecture Kernel Formal Specification

Examples

Proofs Proof Basics Equality Proofs Verified Functions

Effects and Validation Handler-Swap Validation

Surface Languages Surface STLC STLC Core Surface STLC Sums and Products STLC Recursive Lists STLC Refinements and Diagnostics

Applications Category Theory Expression Interpreter Build Simulator

API Reference

Core API Kernel Comp Binds Trampoline Queue Adapt Pipeline State Thunk Sugar Build Types Experimental Desc-interp Compose Compose-laws Composed-shortcut Composed-shortcut-laws Desc Descind-laws Effects Error Error-shortcut-laws Error-uniform-shortcut-laws State State-shortcut-laws Extract Kernel Trampoline

Diagnostics Positions Error Hints Pretty

Effects State Reader Writer Acc Error Conditions Choice Scope Linear Typecheck HasHandler

Types Foundation Primitives Constructors Refinement Dependent Linear Universe

Streams Core Transform Limit Combine Reduce

Type Checker Term Value Quote Conv Eval _internal Dispatch Check Diag _internal Elaborate Meta _internal Hoas _internal _encoders _forced _indexed Surface Registry Generic Desc Datatype Value Derive Check CheckD Ornaments Verified

Diagnostic Hints DArgSort::universe-mismatch DPiSort::universe-mismatch LevelMaxLhs::type-mismatch LevelMaxRhs::type-mismatch LevelSucPred::type-mismatch ULevel::type-mismatch AnnType::not-a-type JType::not-a-type Motive.PiDom::not-a-type Motive::not-a-type PiCod::not-a-type PiDom::not-a-type DArgBody::not-a-desc DPiBody::not-a-desc DPlusL::not-a-desc DPlusR::not-a-desc DRecTail::not-a-desc MuDesc::not-a-desc AppHead::not-a-function DPiFn::not-a-function Motive::not-a-function OpaqueType::not-a-function DPiFn::type-mismatch DRecIndex::type-mismatch DRetIndex::type-mismatch MuIndex::type-mismatch MuPayload::type-mismatch Elem::inhabitation-failed Field::inhabitation-failed SigmaFst::inhabitation-failed SigmaSnd::inhabitation-failed Tag::inhabitation-failed Elem::refinement-failed Field::refinement-failed SigmaFst::refinement-failed SigmaSnd::refinement-failed Tag::refinement-failed Case::type-mismatch Scrut::type-mismatch AnnTerm::type-mismatch AppArg::type-mismatch JType::type-mismatch OpaqueType::type-mismatch ::unhandled-boot-inl ::unhandled-boot-inr ::unhandled-boot-refl ::unhandled-lam ::unhandled-other ::unhandled-pair ::unhandled-tt

docs/nix-effects/API Reference/Effects/HasHandler

HasHandler

Reference

Auto-generated API reference from nix-effects source.

Check if a handler with given name exists in current scope.

prevTypecheck Foundationnext

kleisli.io kli blog docs source

AI agents:llms.txt·llms-full.txt·mcp·tools: search_docs, get_page, list_projects