typesql が漸進的な型付けを採用する理由#

SQL には長年使われてきたクエリがあります。typesql は、その実行言語を別のものに変えずに検証の層を加えます。注釈のないドキュメントも引き続き有効で、注釈を追加するたびに局所的な検証条件を強めます。

消去の規則#

中核となる型構文は検証専用です。expression satisfies T は消去すると expression になります。型付き CTE のヘッダーは列名を残し、型の部分を除去します。import type は文全体を消去します。

消去では、注釈の範囲外にある元の実行時トークンを維持します。文を再整形したり再コンパイルしたりしません。値、行、副作用を変える可能性のある注釈は、typesql の中核構文には含めません。

検証器はデータベースを開かず、スキーマプロバイダーを受け取ります。プロバイダーには、ライブカタログのスナップショット、リポジトリ内のフィクスチャ、内容を固定したパッケージ環境を使えます。そのため同じクエリをエディター、CI、オフラインツールで検証できます。

根拠が不明なら unknown のままにします。見慣れた列名でも、不足している物理型の根拠を補うことはありません。主キーや非 null の主張には、現在のカタログによる裏付けが必要です。

SQL、パッケージ成果物、論理ビュー環境、型グラフ、診断、出力ドキュメントにはすべて受付時の上限があります。負荷の高い実体化の前に上限を適用します。悪意のある、または破損したプロバイダーが、無制限の再帰、メモリ確保、キャッシュ保持を引き起こすことはできません。

これも意味定義の一部です。上限に達した場合は、有効に見える部分的な型結果ではなく、TS0608 や TS0802 などの安定した拒否を返します。

クエリエラーの主な利用者の 1 つは、自分の SQL を修正するエージェントです。そのため、すべての診断に位置、理由、修正方法、安定したコード、機械可読形式を含めます。「構文エラー」だけでは、人もエージェントも修正を完了できません。

インターフェースとなるのはコードと構造なので、呼び出し側を壊さずにメッセージの表現を改善できます。機械的な修正には正確な範囲と置換内容を含め、意味を変える可能性がある提案は文章で示します。

型付き関数は契約の検証を通過してからコンパイルします。パッケージは内容を固定します。論理ビューは正確な由来を付けて展開してから検証します。ポリシーによるマスクは、許可された実行時ポリシーの境界まで masked<T> のまま維持します。

各機能は根拠や再利用可能な構造を追加しながら、元の約束を守ります。型は不正なクエリを早く拒否する助けになりますが、注釈によって実行されるクエリが別のものになることはありません。