The README makes claims. This file backs them up with concrete implementation pointers.
KRL (pronounced "curl") is the resolution language for QuandleDB. This repository holds its normative specification; the implementation lives in QuandleDB.
KRL provides four operation families: construct, transform, resolve, retrieve. The grammar is specified in spec/grammar.ebnf (114 lines, v0.1.0 draft). The executable fragment (retrieval/candidate) is implemented in quandledb/server/krl/ as a Julia lexer, parser, AST and evaluator.
Caveat: This repository does not contain a parser or evaluator. It holds the normative spec, Idris2 ABI, Zig FFI, examples, and proof obligations. Execution requires a QuandleDB checkout.
-
Implementation:
spec/grammar.ebnf,spec/SURFACES.adoc,quandledb/server/krl/(external) -
Learn more: https://github.com/hyperpolymath/quandledb
KRL has four operation families. The four-verb shape is deliberate: it stops "querying" from becoming the whole identity of the language.
The construction/resolution draft uses | as tensor composition; the retrieval/candidate fragment uses | as stage separator. These are incompatible and must not be concatenated. spec/SURFACES.adoc distinguishes them explicitly.
-
Implementation:
spec/SURFACES.adoc,spec/grammar.ebnfvsquandledb/spec/grammar.ebnf -
Learn more: retrieval boundary decision
Idris2 ABI declarations, Zig FFI shim over the C ABI.
The ABI is declared in Idris2 with 4 %foreign declarations (src/interface/abi/). The Zig FFI compiles to libkrl.a with 3/3 unit tests passing. Any language can call via C ABI.
Caveat: ABI primitives are declared but not yet load-bearing — KR-5 is pending decision.
-
Implementation:
src/interface/Abi/Types.idr,src/interface/Abi/Layout.idr,src/interface/Abi/Foreign.idr,src/interface/ffi/src/main.zig -
Learn more: https://idris2.readthedocs.io, https://ziglang.org
Four
.krlprograms, lexically checked against the grammar bytests/smoke/grammar_smoke.sh(20 checks)
Lexical-level checking ensures examples conform to spec/grammar.ebnf without executing them.
-
Implementation:
tests/smoke/grammar_smoke.sh,examples/*.krl
Executable retrieval-fragment acceptance/rejection corpus in
tests/conformance/retrieval_fragment.jl
Cross-repository corpus runs against a supplied QuandleDB checkout, testing filtered retrieval, heuristic candidate metadata, stronger-assurance refusal, and preservation of empty selections.
-
Implementation:
tests/conformance/retrieval_fragment.jl -
Run:
julia --startup-file=no tests/conformance/retrieval_fragment.jl /path/to/quandledb
These aren’t one-off choices — they’re patterns used across hyperpolymath repos:
| Technology | Also Used In |
|---|---|
Idris2 ABI |
https://github.com/hyperpolymath/tangle, https://github.com/hyperpolymath/quandledb, https://github.com/hyperpolymath/echo-types |
Zig FFI |
https://github.com/hyperpolymath/tangle, https://github.com/hyperpolymath/quandledb |
Groove Protocol |
https://github.com/hyperpolymath/groove, https://github.com/hyperpolymath/verisimdb, https://github.com/hyperpolymath/panic-attack |
RSR Template |
All hyperpolymath repos — Rhodium Standard Repository compliance |
| Path | Proves |
|---|---|
|
Normative grammar v0.1.0 draft (114 lines) |
|
Distinguishes construction/resolution draft vs retrieval fragment |
|
Idris2 ABI declarations (Types, Layout, Foreign) |
|
Lowercase alias for RSR compliance (same content) |
|
Zig FFI shim, compiles to libkrl.a |
|
Generated C headers (gitkeep placeholder) |
|
Example KRL programs (4 known) |
|
Lexical smoke checks (20 checks) |
|
Retrieval fragment conformance corpus |
|
E2E suite (FFI build, ABI correspondence, grammar smoke) |
|
Canonical semantic anchor |
|
Groove manifest, port 6462 |
|
Chainguard Wolfi multi-stage build, digest-pinned |