Why typesql is gradual#

SQL already carries years of working queries. typesql adds a proof layer without turning those queries into a different runtime language. A document with no annotations remains valid; each annotation strengthens a local obligation.

The strip laws#

Core type syntax is check-only. expression satisfies T erases to expression. A typed CTE header keeps its column names and loses the type portions. import type erases as a whole statement.

Erasure preserves the original runtime tokens outside annotation spans. It does not reformat or recompile a statement. If an annotation could change a value, row, or side effect, it is not core typesql syntax.

Types come from evidence#

The checker receives a schema provider rather than opening a database. That provider can be a live catalog snapshot, a checked-in fixture, or a content-pinned package environment. The same query can therefore be checked in the editor, CI, or an offline tool.

Unknown evidence stays unknown. A familiar column spelling never upgrades missing physical type evidence. Primary-key and non-null claims require current catalog proof.

The language stays bounded#

SQL, package artifacts, logical-view environments, type graphs, diagnostics, and output documents all have admission limits. Bounds are enforced before expensive materialization. A hostile or corrupt provider cannot force unbounded recursion, allocation, or retained cache state.

This is part of semantics: a limit yields a stable refusal such as TS0608 or TS0802, never a valid-looking partial type result.

Diagnostics are an interface#

A major consumer of query errors is an agent repairing its own SQL. Every diagnostic therefore carries location, reason, rectification, stable code, and machine form. “Syntax error” is not enough information for a person or an agent to converge.

Message wording can improve without breaking callers because the code and structure are the interface. Mechanical fixes carry exact spans and replacements; suggestions that might change meaning remain prose.

Full features preserve the boundary#

Typed functions compile only after their contracts pass. Packages are content-pinned. Logical views expand with exact provenance before checking. Policy masks remain masked<T> until the authorized runtime policy boundary.

Each feature adds evidence or reusable structure while preserving the original promise: types help Supernova refuse a bad query earlier, but annotations never make a different query run.