Documentation menu

typesql#

typesql adds annotations, packages, typed functions, and precise diagnostics to SQL. Its central guarantee is erasure: remove the type-only syntax and the remaining SQL has the same runtime meaning.

typesql
with paid(customer_id: string!, revenue: decimal(18, 2)!) as (
  select
    customer satisfies string!,
    sum(amount) / 100.0 satisfies decimal(18, 2)!
  from titan.stripe.charges
  where status = 'succeeded' and customer is not null
  group by customer
)
select * from paid

Gradual by construction#

Zero annotations is valid. The checker infers what it can from the lake catalog and reports unknown names, incompatible types, bad function arguments, unsafe nullability, and package failures with stable TS#### codes.

Add an annotation where a contract matters. satisfies checks an expression without casting it. ! records a non-null obligation. Typed CTE headers publish a table shape to the rest of the statement.

Runtime separation#

Annotations never become casts or filters. import type erases completely. A diagnosed document is not rewritten into a different query to make it pass.

Use a runtime cast when you intend conversion. Use typesql syntax when you intend verification.

Where types come from#

The schema provider supplies lake columns, primary-key evidence, system columns, JSON shapes, and policy-mask provenance. Content-pinned packages add named shapes and function signatures without requiring a live source during type checking.

Continue with type annotations, the type reference, or the diagnostic registry.