---
title: Why typesql is gradual
description: See how erasure, schema providers, stable diagnostics, packages, and agent-readable errors shape typesql.
species: concept
---
# 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.