VQL-UT (VQL Ultimate Type-Safe)

Overview

VQL-UT is the next-generation query language for VeriSimDB, designed to satisfy all 10 levels of type safety — the 6 established IO-covered forms and the 4 additional forms identified through our research.

The goal is production-worthy VQL that is provably correct at every layer, from parse to execution. At minimum, this repo serves as a research vehicle for exploring the boundaries of type-safe query languages.

Note	This project was briefly known as "vql" during early discussion. The canonical name is *VQL-UT* (Ultimate Type-Safe). All references to vql, vqlpp, or VQL Plus Plus should be read as VQL-UT. File extension: .vqlut.

Lineage

The 10 type safety levels originate in TypeLL (the core type theory), flow into PanLL (panel framework type safety), and are now applied to database queries as VQL-UT.

TypeLL (type theory core — defines the 10 levels)
   │
   ├──→ PanLL (panel framework type safety)
   │
   └──→ VQL-UT (database query language type safety)
             │
             └──→ VeriSimDB (6-modal execution engine)

The Two-Tier Model

Tier	What	How
VQL	The query language	Parser (ReScript) → AST → execution. What users write.
VQL-UT	The safety pipeline	10 progressive levels. Sits behind VQL, applies automatically. Simple queries short-circuit at L1-L2. Proof-carrying queries (with PROOF clause) go through L9-L10. Invisible to the user except when they add a PROOF clause.

Note

VQL-DT (Dependent Types) was the original name for the proof-carrying execution mode (queries with PROOF clauses). It is not a separate product — it is now folded into VQL-UT’s L9 (Proof Attachment) and L10 (Cross-Cutting) levels. All references to "VQL-DT" in older documentation should be read as "VQL-UT L9-L10".

The 6 proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) remain — they are activated by VQL’s PROOF clause and validated by VQL-UT levels L9-L10.

Adoption Strategy

The type safety story unfolds in three phases:

1. ReScript evangeliser proves the concept first — demonstrate the value of these type safety levels in ReScript itself, where the developer community can experience them firsthand

2. Once proven, VQL-UT and AffineScript become the two showcase languages for teaching people the 10 levels of type safety

3. VQL-UT handles the database query domain; AffineScript handles general-purpose programming

The 10 Levels of Type Safety

Established (IO-Covered) — 6 Levels

Level	Name	Description
1	Parse-time safety	Query syntax verified at parse time — malformed queries rejected before processing
2	Schema-binding safety	Column names, table references, relationships validated against live schema
3	Type-compatible operations	Arithmetic, comparison, aggregation only on compatible types
4	Null-safety	Nullable vs non-nullable tracked through joins, subqueries, projections
5	Injection-proof safety	Parameterised queries enforced at type level — interpolation impossible by construction
6	Result-type safety	Query return types known at compile time — no runtime casting

Research-Identified — 4 Additional Levels

Level	Name	Description
7	Cardinality safety	Return count guarantees (exactly-one, at-most-one, many) in the type system
8	Effect-tracking safety	Read vs write vs DDL distinguished at type level — pure queries cannot mutate
9	Temporal safety	Bi-temporal and system-time queries carry time bounds in types — prevents stale reads
10	Linearity safety	Connection and transaction handles are linear types — use-after-close impossible

TypeQL-Experimental Extension Mechanisms (Levels 7-10)

The typeql-experimental sub-project within nextgen-databases prototyped 6 mechanisms that map to levels 7-10:

Mechanism	VQL-UT Syntax	Idris2 Encoding
Linear types	CONSUME AFTER N USE	QTT quantity 1 on Connection
Session types	WITH SESSION protocol	Session : SessionState → Type indexed type
Effect systems	EFFECTS { Read, Write }	Effect set with subsumption proofs
Modal types	IN TRANSACTION	Box types indexed by world/scope
Proof-carrying code	PROOF ATTACHED theorem	ProvedResult sigma type
Quantitative type theory	USAGE LIMIT n	Bounded resource tracking via QTT

Architecture

                        +---------------+
                        |  VQL Source   |
                        |  (.vqlut)     |
                        +-------+-------+
                                |
                    +-----------v-----------+
                    |  Parser (Level 1)     |  ReScript — extends VeriSimDB VQL parser
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Schema Binder (2)    |  Idris2 — dependent types on schema
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Type Checker (3-6)   |  Idris2 — nullability, injection, results
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Effect Analyser      |  Idris2 — cardinality (7), effects (8),
                    |  (7-10)               |           temporality (9), linearity (10)
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Zig FFI Codegen      |  Compiles to C-ABI query plan
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  VeriSimDB Engine     |  6-modal execution
                    +-----------------------+

Technology Stack

Layer	Language	Purpose
Core type system	Idris2	Dependent types for all 10 safety levels. %default total.
FFI bridge	Zig	C-ABI query plan compilation. Zero-copy result sets.
Parser	ReScript	Surface syntax parsing, extending VeriSimDB’s VQL parser.
API layer	V-lang	REST/gRPC/GraphQL endpoints for query submission.
VeriSimDB integration	Elixir	6-modal storage engine connection via NIFs.

Roadmap

Phase 1 — Foundation (Levels 1-3)

• ❏ VQL-UT grammar specification (EBNF, extending VQL v3.0)

• ❏ Idris2 parser with totality proof

• ❏ Schema representation as dependent types

• ❏ Type-compatible operation checker

• ❏ Zig FFI for query plan emission

• ❏ Basic test suite against VeriSimDB

Phase 2 — Safety Core (Levels 4-6)

• ❏ Null-tracking through join algebra

• ❏ Injection-proof parameterisation (type-level enforcement)

• ❏ Result-type inference with compile-time guarantees

• ❏ Property-based tests (QuickCheck/Hedgehog)

Phase 3 — Research Levels (Levels 7-10)

• ❏ Cardinality annotations and inference

• ❏ Effect system (Read/Write/DDL monad stack)

• ❏ Temporal type annotations for bi-temporal queries

• ❏ Linear types for connections and transactions (Idris2 QTT)

Phase 4 — Production Hardening

• ❏ Performance benchmarks against raw SQL

• ❏ VeriSimDB 6-modal query planner integration

• ❏ ReScript client SDK with type generation

• ❏ Documentation and specification publishing

Related Projects

Project	Relationship
nextgen-databases/verisimdb	Target database engine (6-modal octad storage)
nextgen-databases/verisimdb/docs/VQL-SPEC.adoc	Base VQL grammar specification (26KB, EBNF appendix)
nextgen-databases/verisimdb/docs/vql-vs-vql-dt.adoc	VQL-DT specification (to be superseded by VQL-UT)
nextgen-databases/typeql-experimental	6 extension mechanisms for levels 7-10 (Idris2 kernel + ReScript parser)
typell	Core type theory — the 10 levels originate here
panll	Panel framework — integrates TypeLL type safety for UI
nextgen-languages/affinescript	Sister showcase for type safety adoption (general-purpose programming)

Building

# Type-check the Idris2 core
cd src/interface/abi && idris2 --typecheck

# Build FFI
cd src/interface/ffi && zig build

# Run tests
just test

License

PMPL-1.0-or-later