feat: add typeql-experimental (VQL-dt++) — 6 type-theoretic extensions to VQL

Implement experimental exploration of linear types, session types, effect
systems, modal types, proof-carrying code, and quantitative type theory
as extensions to VQL (VeriSim Query Language).

Idris2 kernel: 9 modules type-check clean with %default total and zero
banned patterns (no believe_me/assert_total/assert_smaller). Zig FFI
bridge: 5 tests pass on Zig 0.15.2. ReScript parser written following
VeriSimDB combinator patterns. 7 annotated .vqlpp example files.

Also updates parent README.adoc with revised project descriptions and
priority notes for VeriSimDB, LithoGlyph, and QuandleDB.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/STATE.scm

@@ -1,8 +1,9 @@
 ;; SPDX-License-Identifier: PMPL-1.0-or-later
-(state (metadata (version "0.1.0") (last-updated "2026-02-13") (status active))
-  (project-context (name "nextgen-databases") (purpose "Parent repo tracking database application portfolio") (completion-percentage 30))
+(state (metadata (version "0.3.0") (last-updated "2026-03-01") (status active))
+  (project-context (name "nextgen-databases") (purpose "Parent repo tracking database application portfolio") (completion-percentage 35))
   (components
     (component "quandledb" (status "active") (description "Knot-theory database wrapping Skein.jl"))
     (component "verisimdb" (status "active") (description "Multimodal verification database"))
     (component "lithoglyphdb" (status "active") (description "Glyph and inscription database"))
-    (component "glyphbase" (status "planned") (description "Web frontend for LithoglyphDB"))))
+    (component "glyphbase" (status "planned") (description "Web frontend for LithoglyphDB"))
+    (component "typeql-experimental" (status "active") (description "VQL-dt++ experimental type-theoretic extensions — 9/9 Idris2 modules type-check, 5/5 Zig FFI tests pass, ReScript parser written"))))

README.adoc

@@ -24,32 +24,39 @@ This repository serves as the central tracking hub for the Next-Gen Databases in
 |===
 | Database | Description | Technology | Query Language | Status
 
+| *VeriSimDB*
+| Cross-system entity consistency engine — 8 modalities (octad), drift detection, self-normalisation, formally verified queries. **Primary database project.** Operates as standalone database OR federation coordinator over existing databases (PostgreSQL, ArangoDB, Elasticsearch).
+| Rust (core) + ReScript (VQL parser) + Elixir (orchestration)
+| VQL (VeriSim Query Language) + VQL-DT (dependent types)
+| Active — beta
+
 | *QuandleDB*
-| Knot-theory database — stores knots as Gauss codes, computes invariants (Jones polynomial, genus, Seifert circles), queries by topological properties
+| Knot-theory database — stores knots as Gauss codes, computes invariants (Jones polynomial, genus, Seifert circles), queries by topological properties. **Exploratory/research project**: a thought experiment in applying knot theory to database design, not yet intended as a production tool.
 | Julia (Skein.jl engine) + ReScript frontend
 | KQL (Knot Query Language) — in development
-| Active
+| Exploratory
 
-| *VeriSimDB*
-| Multimodal verification database — 6 modalities (Graph, Vector, Tensor, Semantic, Document, Temporal) for security analysis and software verification
-| Rust (core) + ReScript (VQL parser) + Elixir (executor)
-| VQL (Verification Query Language)
-| Active
-
-| *LithoglyphDB*
-| Glyph and inscription database — catalogues lithographic specimens, inscriptions, and symbol systems with provenance tracking
-| Rust + Julia
-| (planned)
-| Active
+| *LithoGlyph*
+| Narrative-first, reversible, audit-grade database core for journalism, narrative arts, and media/comms. Working towards production but **secondary priority** to VeriSimDB. Long-term vision: intimate integration with portfolio tools (bofig, etc.) for journalism and PR applications.
+| Forth (storage) + Zig (bridge) + Factor (FQL) + Idris2 (proofs) + Lean 4 (normalizer)
+| GQL (Glyph Query Language) — planned
+| Active — on backburner
 
 | *Glyphbase*
-| Web interface for LithoglyphDB — browser-based search, visualisation, and annotation of glyph specimens
-| ReScript frontend + LithoglyphDB API
-| (via LithoglyphDB)
+| Web interface for LithoGlyph — browser-based search, visualisation, and annotation of glyph specimens
+| ReScript frontend + LithoGlyph API
+| (via LithoGlyph)
 | Planned
 
 |===
 
+[NOTE]
+====
+**Project priorities:** VeriSimDB is the primary database engineering project, receiving active development focus. LithoGlyph is working towards production for specialist use in journalism and narrative arts, but is secondary priority while VeriSimDB matures. QuandleDB is a research exploration into knot theory's applications in database design — valuable for the mathematical insights but not positioned as a production tool at this stage.
+
+Lessons learned from VeriSimDB development (drift detection, formal verification, federation) will directly improve LithoGlyph when development focus returns to it.
+====
+
 == Architecture
 
 Each database in the portfolio follows a layered architecture:

typeql-experimental/.gitignore

@@ -0,0 +1,11 @@
+# Idris2 build artefacts
+build/
+
+# Zig build artefacts
+ffi/zig/.zig-cache/
+ffi/zig/zig-out/
+
+# ReScript build artefacts
+lib/
+node_modules/
+.merlin

typeql-experimental/.machine_readable/ECOSYSTEM.scm

@@ -0,0 +1,52 @@
+;; SPDX-License-Identifier: PMPL-1.0-or-later
+(ecosystem
+  (version "1.0.0")
+  (last-updated "2026-03-01")
+
+  (name "typeql-experimental")
+  (type "experimental-language-extension")
+  (purpose "Explore advanced type-theoretic extensions to VQL")
+
+  (position-in-ecosystem
+    (parent "nextgen-databases"
+      (relationship "sub-project")
+      (description "Lives within the nextgen-databases monorepo, no own .git"))
+    (description "Experimental sister project to VQL-dt. While VQL-dt is the
+                  production dependent type system for VeriSimDB (~35% wired),
+                  typeql-experimental explores six advanced extensions that may
+                  eventually feed back into VQL-dt. All 9 Idris2 modules
+                  type-check clean with zero banned patterns."))
+
+  (related-projects
+    (project "verisimdb"
+      (relationship "sibling-dependency")
+      (description "VQL v3.0 grammar (317 lines), VQL-dt type checker,
+                    AST types, parser combinator patterns. Primary reference.")
+      (artefacts-used "vql-grammar.ebnf" "VQLParser.res" "VQLTypes.res"))
+
+    (project "lithoglyph"
+      (relationship "sibling-pattern")
+      (description "GQL-dt (FBQLdt) Idris2 ABI patterns. ipkg structure,
+                    module organisation, zero-believe_me invariant.")
+      (artefacts-used "fbqldt.ipkg" "src/FormBD/*.idr"))
+
+    (project "proven"
+      (relationship "potential-consumer")
+      (description "Formal verification library. Proof-carrying code extension
+                    may integrate with proven's certificate format."))
+
+    (project "quandledb"
+      (relationship "sibling-inspiration")
+      (description "Knot-theory database. KQL query language may benefit from
+                    similar type extensions."))
+
+    (project "nqc"
+      (relationship "sibling-tool")
+      (description "NQC cross-database console. Web UI patterns (ReScript + Deno)
+                    informed the parser build setup.")))
+
+  (technologies
+    (technology "Idris2" (role "type-system-kernel") (version "0.8.0"))
+    (technology "ReScript" (role "parser") (version ">= 11.0"))
+    (technology "Deno" (role "runtime") (version ">= 2.0"))
+    (technology "Zig" (role "ffi-bridge") (version "0.15.2"))))

typeql-experimental/.machine_readable/META.scm

@@ -0,0 +1,83 @@
+;; SPDX-License-Identifier: PMPL-1.0-or-later
+(meta
+  (version "1.0.0")
+  (last-updated "2026-03-01")
+
+  (architecture-decisions
+    (decision "vql-not-sql"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Need a base query language for type extensions")
+      (decision "Use VQL (VeriSim Query Language) as foundation, not SQL")
+      (rationale "VQL's cross-modal semantics (HEXAD, 8 modalities, PROOF clauses)
+                  are the natural foundation. SQL's relational model is too flat
+                  for the properties we want to prove."))
+
+    (decision "idris2-qtt-native"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Need linear types for resource-counted connections")
+      (decision "Use Idris2's native QTT (quantitative type theory) rather than encoding linearity")
+      (rationale "Idris2 variables carry quantities (0, 1, omega). CONSUME AFTER 1 USE
+                  maps to (1 conn : Connection) — compiler enforces linearity for free."))
+
+    (decision "delta-grammar"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Need grammar for 6 new clause types")
+      (decision "Extend VQL v3.0 EBNF with optional clauses appended after standard query")
+      (rationale "No keyword conflicts. All new keywords disjoint from VQL's 60+ reserved words."))
+
+    (decision "dual-language-split"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Need both formal proofs and practical parsing")
+      (decision "Idris2 for type kernel, ReScript for parser")
+      (rationale "Idris2 proves properties. ReScript parses queries. Independent operation
+                  in experimental phase — no runtime interop needed."))
+
+    (decision "zero-believe-me"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Formal verification integrity")
+      (decision "Absolute ban on believe_me, assert_total, assert_smaller")
+      (rationale "These undermine formal verification. If a proof cannot be
+                  completed, the type definition must be restructured."))
+
+    (decision "zig-0-15-build-api"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Zig 0.15.2 removed addStaticLibrary from Build API")
+      (decision "Use addModule + addTest(.root_module) pattern instead of addStaticLibrary")
+      (rationale "Zig 0.15 restructured the build system. Module-based approach
+                  is the idiomatic pattern. build.zig.zon required for package metadata."))
+
+    (decision "subsumes-argument-order"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Effect subsumption direction was initially backwards")
+      (decision "Subsumes declared actual = Subset actual declared (actual is subset of declared)")
+      (rationale "A query's actual effects must be a subset of its declared effects.
+                  The original direction (Subset declared actual) was backwards,
+                  meaning 'every declared effect appears in actual' which is wrong."))
+
+    (decision "no-erased-pattern-match"
+      (status accepted)
+      (date "2026-03-01")
+      (context "Idris2 quantity-0 implicits cannot be pattern-matched at runtime")
+      (decision "Removed hasUses function; use type system to distinguish Available from Depleted")
+      (rationale "Erased (quantity 0) implicits exist only at type level. Any function
+                  that needs to inspect the resource count must take it as a runtime argument.")))
+
+  (development-practices
+    (practice "all-modules-total"
+      (description "Every Idris2 module uses %default total"))
+    (practice "structural-termination"
+      (description "All recursive functions prove termination structurally"))
+    (practice "parser-combinator-pattern"
+      (description "ReScript parser follows VeriSimDB's combinator style"))
+    (practice "ipkg-typecheck"
+      (description "Use 'idris2 --typecheck file.ipkg' for packages, not --check"))
+    (practice "explicit-nesting"
+      (description "Non-associative helper functions (andCheck) require explicit nested calls,
+                    not backtick infix chaining"))))

typeql-experimental/.machine_readable/STATE.scm

@@ -0,0 +1,107 @@
+;; SPDX-License-Identifier: PMPL-1.0-or-later
+(state
+  (metadata
+    (version "1.0.0")
+    (last-updated "2026-03-01")
+    (status active))
+
+  (project-context
+    (name "typeql-experimental")
+    (purpose "Experimental type-theoretic extensions to VQL (VQL-dt++)")
+    (completion-percentage 85))
+
+  (current-position
+    (phase "initial-implementation-complete")
+    (summary "All 37 files implemented across 6 phases. Idris2 kernel (9 modules)
+              type-checks clean with --total and zero banned patterns. Zig FFI
+              bridge (5 tests) passes. ReScript parser and examples written.
+              Six extensions: linear types, session types, effect systems,
+              modal types, proof-carrying code, quantitative type theory."))
+
+  (components
+    (component "idris2-kernel"
+      (status "complete")
+      (description "9 Idris2 modules: Core, Linear, Session, Effects, Modal,
+                    ProofCarrying, Quantitative, Checker, Proofs. All type-check
+                    with %default total. Zero believe_me/assert_total/assert_smaller.")
+      (completion 100))
+    (component "rescript-parser"
+      (status "written")
+      (description "Extended AST (TQLAst.res) and parser (TQLParser.res) for 6 new
+                    VQL++ clauses. Follows VeriSimDB combinator patterns. Not yet
+                    build-tested (requires rescript-legacy toolchain).")
+      (completion 70))
+    (component "grammar-spec"
+      (status "complete")
+      (description "Delta EBNF extending VQL v3.0 with 6 new clause types.
+                    Documented in docs/vql-dtpp-grammar.ebnf.")
+      (completion 100))
+    (component "zig-ffi"
+      (status "complete")
+      (description "C-compatible FFI bridge skeleton. build.zig targets Zig 0.15.2.
+                    5 tests pass: empty annotations, consume_after=0, usage<consume,
+                    full valid annotations, version string.")
+      (completion 100))
+    (component "examples"
+      (status "complete")
+      (description "7 annotated .vqlpp example files covering all 6 extensions
+                    individually plus a combined maximal query.")
+      (completion 100))
+    (component "idris2-tests"
+      (status "complete")
+      (description "3 compile-time test modules: TestLinear.idr, TestSession.idr,
+                    TestQuantitative.idr. Validated by Idris2 type-checker.")
+      (completion 100))
+    (component "documentation"
+      (status "complete")
+      (description "README.adoc, DESIGN doc, type-system-spec.adoc, examples.adoc,
+                    grammar EBNF, AI manifest, machine-readable SCM files.")
+      (completion 100)))
+
+  (route-to-mvp
+    (milestone "type-kernel-complete"
+      (description "All 9 Idris2 modules type-check with --total, zero believe_me")
+      (completion 100))
+    (milestone "zig-ffi-tested"
+      (description "Zig FFI bridge compiles and all 5 tests pass on Zig 0.15.2")
+      (completion 100))
+    (milestone "parser-written"
+      (description "ReScript parser written with combinator pattern from VeriSimDB")
+      (completion 70))
+    (milestone "parser-build-tested"
+      (description "ReScript parser compiles and accepts all 7 example .vqlpp files")
+      (completion 0))
+    (milestone "integration"
+      (description "Idris2 proofs validated against ReScript-parsed ASTs")
+      (completion 0)))
+
+  (verified-results
+    (result "idris2-typecheck"
+      (command "idris2 --typecheck typeql-experimental.ipkg")
+      (outcome "9/9 modules compile clean")
+      (date "2026-03-01"))
+    (result "zig-tests"
+      (command "cd ffi/zig && zig build test")
+      (outcome "5/5 tests pass")
+      (date "2026-03-01"))
+    (result "banned-patterns"
+      (command "grep -rn 'believe_me|assert_total|assert_smaller' src/abi/")
+      (outcome "zero matches (comment-only reference in Proofs.idr)")
+      (date "2026-03-01")))
+
+  (implementation-notes
+    (note "idris2-version" "Idris2 0.8.0 — ipkg uses --typecheck not --check")
+    (note "zig-version" "Zig 0.15.2 — addModule/addTest API, no addStaticLibrary")
+    (note "effects-subsumption" "Subsumes declared actual = Subset actual declared (flipped)")
+    (note "erased-implicit" "Cannot pattern-match on quantity-0 implicits (removed hasUses)")
+    (note "andCheck-nesting" "Non-associative function requires explicit nested calls"))
+
+  (blockers-and-issues
+    (blocker "rescript-build"
+      (description "ReScript parser not yet build-tested — needs rescript-legacy or
+                    equivalent toolchain. Written code follows VeriSimDB patterns.")))
+
+  (critical-next-actions
+    (action "Build-test ReScript parser with rescript-legacy toolchain")
+    (action "Test all 7 example .vqlpp files parse correctly")
+    (action "Wire Idris2 proof results to ReScript-parsed ASTs (integration phase)")))