QuandleDB: query language design (SQL + dependent type variants) #4

Activity

1. hyperpolymath

   added a commit that references this issue on Mar 20, 2026

   feat: update quandledb — KQL query language design complete (closes #4)

   ...

   This issue will close once commit 05e845c is merged into the 'main' branch.

   05e845c
2. hyperpolymath commented on Mar 20, 2026

   

   hyperpolymath

   on Mar 20, 2026

   OwnerAuthor

   More actions

   Resolved in 05e845c on chore/cicd-optimizations:

   KQL Query Language Design — SQL + Dependent Type Variants

   New spec documents:

   • spec/sql-compat.md — SQL→KQL translation rules: SELECT→return, WHERE→filter, ORDER BY→sort, LIMIT→take, GROUP BY→group_by. Documents supported/unsupported SQL features and implementation strategy as syntactic frontend.
   • spec/dependent-type-variants.md — Five dependent type variants:
     1. Dependent projection (return clause determines record type)
     2. Confidence-indexed equivalences (Equivalence[Knot, Exact])
     3. Invariant-dependent records (via clause determines evidence types)
     4. Stratum-bounded evaluation (Nat-indexed termination proof)
     5. Pipeline composition (type-safe stage chaining)

   Idris2 ABI updates (src/abi/Types.idr):

   • Filled combinePreservesInvariants proof hole
   • Added ConfEquiv (confidence-indexed equivalence type)
   • Added HasField/ProjectFields (dependent projection proofs)
   • Added InvType registry (type-level invariant→type mapping)
   • Added StratEval with stratCountCorrect termination proof

   Grammar (spec/grammar.ebnf):

   • Added Equivalence[τ, confidence] and ResultSet[τ] type annotations
   • Added SQL compatibility syntax (SELECT/FROM/WHERE/GROUP BY/ORDER BY/LIMIT)
3. hyperpolymath

   closed this as completedon Mar 20, 2026
4. hyperpolymath

   added a commit that references this issue on Mar 20, 2026

   feat: update quandledb — KQL query language design complete (closes #4)

   ...

   This issue will close once commit 519e45a is merged into the 'main' branch.

   519e45a
5. hyperpolymath

   added 2 commits that reference this issue on Jul 21, 2026

   Record GNPL re-scope: narration/projection; core-factor/gql superseded (

   ...

   522c7a2

   Remove the extracted lithoglyph tree — it existed in two places (#58)

   ...

   c42ed14
6. hyperpolymath

   added a commit that references this issue on Sep 25, 2026

   Foundational fixes for #42, #45, #53 — template debt, migration, veri…

   ...

   fc12a2e