VCL-total (VeriSim Consonance Language — Total Type-Safe)

Important

This project was renamed on 2026-04-05. Its former name used the letter sequence "V-Q-L-hyphen-U-T" (read: "vee-queue-ell-you-tee") and stood for "Ultimate Type-safe". The canonical name is now VCL-total (VeriSim Consonance Language — Total Type-safe). See CHANGELOG.md for the full rename scope. The GitHub repository URL is unchanged.

Table of Contents

• Overview
• Lineage
  • The Two-Tier Model
  • Adoption Strategy
• The 10 Levels of Type Safety
  • Established (IO-Covered) — 6 Levels
  • TypeQL-Experimental Extension Mechanisms (Levels 7-10)
• Architecture
• Technology Stack
• Roadmap
  • Phase 1 — Foundation (Levels 1-3)
  • Phase 2 — Safety Core (Levels 4-6)
  • Phase 3 — Advanced Safety (Levels 7-10)
• Related Projects

Overview

VCL-total is the next-generation interaction language for Verisim (engine formerly known in discussion as 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 -total suffix denotes totality in the dependent-type sense: no partial functions, no undefined behaviour at type level.

The goal is production-worthy VCL 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 interaction languages for consonance engines.

Note	Verisim operations are propositions to a consonance engine, not queries against a passive store. Operations split into propositional (DECLARE, ASSERT, RETRACT) and epistemic (INSPECT, VERIFY). "Query language" is therefore a misnomer; "consonance language" names the actual thing.

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 consonance statements as VCL-total.

TypeLL (type theory core — defines the 10 levels)
   │
   ├──→ PanLL (panel framework type safety)
   │
   └──→ VCL-total (consonance-statement type safety)
             │
             └──→ Verisim (8-modal octad consonance engine)

The Two-Tier Model

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

Note	The dependent-types variant was originally labelled with the suffix "-DT" (Dependent Types) as the proof-carrying execution mode (statements with PROOF clauses). It is not a separate product — it is folded into VCL-total’s L9 (Proof Attachment) and L10 (Cross-Cutting) levels.

The 6 proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) remain — they are activated by VCL’s PROOF clause and validated by VCL-total 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, VCL-total and AffineScript become the two showcase languages for teaching people the 10 levels of type safety

3. VCL-total handles the database-interaction domain; AffineScript handles general-purpose programming

The 10 Levels of Type Safety

Established (IO-Covered) — 6 Levels

Level	Name	Description
L1	Syntactic parsability	Parser accepts the input.
L2	Well-formedness	Structure matches the grammar.
L3	Schema conformance	References resolve to declared entities.
L4	Type compatibility	Operator arities and types align.
L5	Nullability tracking	NULL propagates explicitly through joins.
L6	Injection resistance	Parameterisation and escaping are type-level invariants.

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	VCL-total 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

                        +---------------+
                        |  VCL Source   |
                        |  (.vcltotal)  |
                        +-------+-------+
                                |
                    +-----------v-----------+
                    |  Parser (Level 1)     |  ReScript — extends Verisim VCL parser
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Schema Binder (2)    |  Idris2 — dependent types on schema
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Type Checker (3-6)   |  Idris2 — nullability, injection, results
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Safety Checker (7-10)|  Idris2 — linear, session, effects, proofs
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  FFI Bridge           |  Zig — C-ABI, zero-copy plan emission
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Verisim              |  8-modal octad storage engine
                    +-----------------------+

Technology Stack

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

Roadmap

Phase 1 — Foundation (Levels 1-3)

• ❏ VCL-total grammar specification (EBNF, extending VCL v3.0)

• ❏ Idris2 parser with totality proof

• ❏ Schema representation as dependent types

• ❏ Type-compatible operation checker

• ❏ Zig FFI for plan emission

• ❏ Basic test suite against Verisim

Phase 2 — Safety Core (Levels 4-6)

• ❏ Null-tracking through join algebra

• ❏ Injection-resistant parameterisation

• ❏ Integration with Verisim’s 8-modal execution

Phase 3 — Advanced Safety (Levels 7-10)

• ❏ Linear resource tracking (QTT)

• ❏ Session-typed protocols

• ❏ Effect inference

• ❏ Proof-attached statement execution

Related Projects

Project	Relationship
verisimdb	Target consonance engine (8-modal octad storage)
verisimdb/docs/VCL-SPEC.adoc	Base VCL grammar specification (EBNF appendix)
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 applying the same 10 levels to UI type safety