Parsers, interpreters, etc.

A dependently typed proof checker

data Nat : Type {
  zero : Nat;
  succ : Nat -> Nat;
}

// succ zero equals one, by computation.
val one : Nat = succ zero

A proof checker for the Calculus of Inductive Constructions, with an ML-family surface syntax. You write data types, functions, and proofs; Doxa checks that the proofs actually establish the theorems you state. Rumil parses the source into a surface tree; the elaborator, type checker, and normalizer are Doxa's own. It compiles to WebAssembly and runs entirely in the browser, with no server, in about 76KB. Preview: the kernel is complete and the standard library type-checks end to end, but the language is still settling and has not had a tagged release.

• Dependent types over a predicative universe hierarchy with an impredicative Prop
• Inductive types with parameters, indices, and auto-derived recursors
• Dependent pattern matching with structural-recursion checking
• Propositional equality with definitional proof irrelevance
• Type errors that point at the offending term with the names you wrote
• Stack-safe, linear-time kernel operations, verified to a million levels deep

A shape-aware query language

$ lam '.dependencies | keys' pubspec.yaml
["rumil", "rumil_parsers", "args"]
$ lam '.services | values | map(.image)' docker-compose.yaml
["postgres:16", "redis:7-alpine"]
$ lam '.user.name' config.toml
"hakim"

A query language for JSON, YAML, TOML, HCL, CSV, and Markdown that shows you what you're working with. Expressions compose through the pipe operator, and `--explain` reports the shape of the data at each stage of the pipeline, before you run it. It takes JSON Schema as input, bridges between formats, and ships as a CLI, a Dart library, and an MCP server. Built on Rumil.

• Shape-aware `--explain` reports the structure at each pipeline stage before running
• Same query syntax across JSON, YAML, TOML, HCL, CSV, and Markdown
• Format bridges and JSON Schema input
• Null propagation on navigation, strict on computation
• CLI, Dart library, and MCP server for AI assistants

Parser combinators with lossless syntax trees

// Describe what to parse. Nothing runs yet.
final id = letter & (letter | digit).many;
final assign = id & char('=').trim & expr;

// The interpreter handles the rest.
final result = assign.parse('x = 42');

A parser combinator library that represents parsers as data, not functions. You describe what to parse; a separate interpreter handles backtracking, operator precedence, and error reporting. Because parsers are values, left-recursive grammars work without rewriting, and deep input stays stack-safe, bounded by memory rather than the call stack. Beyond a parse result, rumil can produce lossless green/red syntax trees with resilient error recovery and incremental reparse, so language tooling can keep a tree in sync as the source is edited.

• Lossless green/red syntax trees with resilient recovery and incremental reparse
• Operator precedence through `pratt`, a Pratt parser expressed as a combinator
• Stack-safe to arbitrary depth, bounded by memory rather than the call stack
• Success, Partial, Failure. Error recovery is part of the result type
• Paired with rumil_parsers (JSON, YAML, TOML, XML, CSV, HCL, Proto3, Markdown) and rumil_tokens

Validators derived at compile time

val user = (
  field("name", nonEmpty),
  field("age", between(0, 150)),
  field("email", matches(emailPattern))
).zip  // collects all errors in one pass

user.validate(input)

A validation library for Scala 3 that derives validators from your types at compile time. If a field type is missing a validator, the compiler reports every missing one, names the fields, and tells you what to add. Validators compose in two modes: zip to collect all errors in one pass, flatMap to stop at the first. Errors carry field paths, so failures point to the exact location in nested data.

• Compile-time derivation through Scala 3 inline macros and Mirror types
• Error accumulation with zip, fail-fast with flatMap
• Structured errors with field paths, severity, and error codes
• Cross-compiles to JVM and Scala Native