構造的正確性

ブログ / 構造的正確性 構造的正確性 2026.06.27 ~6分読了 型システムは素晴らしいものです。コンパイル時に多くのバグを捕捉し、アプリケーションのフォワード開発のための文法/語彙に貢献します。型システムと同様に、現代の正確性検証ツールは、ドメインのグラフ構造モデルを介して、問題の構造的記述を活用します。 型システムは、プログラムを型、関数、トレイトなどのグラフとそれらの関係として記述します。型がノードであり、戻り値、引数、実装などの関係がエッジです。 Bazelのようなビルドシステムは、ビルドターゲットをノードとし、依存関係をそれらの間のエッジとして持ちます。明示的な依存関係が記述されていない場合、他の手段でビルドされたとしても、記述されていないパッケージはビルドターゲットに提供されず、ハーメティシティと自明なデプロイ可能性を実現します。 インターフェース記述言語は、メッセージ型とサービスをノードとし、戻り値の型とパラメータの型をエッジとします（制限された型システム）。 データベースは、外部キー（エッジ）を使用して、関連するテーブル行（ノード）間の関係を記述します。ただし、データベースはチェック制約も使用して正確性を実装します。これは構造的ではありませんが、加法的に記述できない側面を表現するための有用な述語です。 構造的正確性 ドメインを型付きノードとエッジのグラフとしてモデル化します。これらのグラフの最良のものは定義的です。システムを記述する構造がシステムそのものです。エッジがなければ、機能もありません。各ドメインには独自のノードとエッジの型語彙があります。Bazelは、異なるエッジの型による豊かさの良い例です。depsは「このコードをリンクする」を意味し、srcsは「これらのファイルをコンパイルする」を意味し、dataは「実行時に利用可能にする」を意味します。それぞれがターゲットグラフ内の異なるエッジ型であり、それぞれが異なる機能を構成します。ノードとエッジの型をエレガントに選択することで、表現力豊かで強力なツールが生まれます。 これらの正確性ツールの多くは、構造的正確性と述語の両方を活用して、有効な構成を記述します。これらのグラフ構造システムの最良のものは、構成的/定義的です。それらは「何が有効か」と「出力がどのように計算されるか」の両方を定義します。Bazelでは、ターゲットは依存しないモジュールをインポートできません。これにより、2つの貴重な機能が提供されます。(a)システムが機能するためには検証可能な不変条件が記述されなければならないため、デフォルトで検証可能なシステムが構築され、(b)記述された属性と関係が動作と検証の両方の役割を果たすため、仕様の簡潔さが得られます。Bazelプロジェクトをビルドすることで、製品の明示的な構造を記述することを余儀なくされ、開発を継続しながらそれを検証する手段を得ることができます。この「各ドメインには独自の名詞と動詞がある」という点と、「定義的なグラフ構造システム」という点が、Bazelが製品全体を記述するための優れた基盤である理由です。 Bazelを使用すると、ドメインの概念（パッケージ、サービス、データセット）の任意のノード型を定義し、型付きエッジを介してそれらの関係を制約し、その単一の構造的記述からビルド/テスト/デプロイパイプライン全体を導出できます。サービス、そのメトリクスエンドポイント、およびそれをスクレイプするPrometheusデプロイメントはすべて同じグラフのノードとなり、それらの関係は一度宣言され、システム全体をコンパイル、デプロイ、検証するために使用されます。 しかし、状態についてはどうでしょうか？良い質問です！データベースは、スキーマで指定されたテーブル、外部キー、チェック制約を介して格納できるものを定義します。しかし、それら以外では有効な状態遷移を特定しません。これはしばしばアプリケーション層に任され、HTTPまたはRPCエンドポイントがビジネスロジックを忠実に実装するために頼られます。しかし、これはしばしば問題が発生する場所です。たとえば、両方とも注文ステータスを変更する2つのエンドポイントがあり、一方が出荷済みにする前に在庫チェックを忘れるなどです。 カラーペトリネット（CPN）は、スキーマで指定されたコレクション（プレイス/トークン）を受け取り、遷移を介して厳密な「次の状態」定義を追加します。CPNでは、特定のバインディングが選択され、その遷移が発火し、特定のプレイスでトークンを消費、変異、生成することによってのみ状態が変化します。これはグラフ構造システムを状態に適用したものです。プレイスと遷移がノードであり、それらを接続するアークがエッジです。Bazelと同様に、CPNシステムの機能を定義する概念は、システムをより完全に検証する手段としても二重の役割を果たします。 CPNがこれをどのように行うかを示すために、かなり複雑な例であるWebスクレイパーを見てみましょう。私は元のCPNの投稿で関心のあるアプリケーションとして記述したWebスクレイパーを実装しました。この例では、スクレイパーはプロキシのローテーションセットを使用する必要があり、サイトの過負荷を防ぐためにドメインの「リース」セマンティクスを実装する必要があります。伝統的に、このようなステートフルシステムを構築することは、複数の層にわたって調整を分散させることを意味します。データベースはリソースの状態を処理し（SELECT FOR UPDATEと注意深いロック順序付けを介して）、タスクキューはジョブスケジューリングを処理し、アプリケーションコードはレート制限とクールダウンロジックを処理し、さらに別のコンポーネントがドメイン同時実行制限を強制します。それぞれが不完全な正確性のビューを持っています。そして、チェック制約、単体テスト、アプリケーションレベルの述語を記述し、試行錯誤を通じてそれらが一致するようにすることで信頼性を高めます。 CPNでは、スクレイパーの調整モデル全体がトークンと遷移として宣言されます。スクレイピングのためにリソースを要求することは、利用可能なリソース、プロキシ、およびドメインの状態にわたってバインドする単一の遷移（select_resource）です。それは、プロキシをアトミックにリースし、ドメインのアクティブカウントを増やし、セッションをすべて同じ発火で作成します。正しいロック戦略は必要ありません。なぜなら、バインディングシステムは有効な組み合わせのみが参加することを保証するからです。プロキシの保存はテストする特性ではありません。なぜなら、それはトポロジカルな事実だからです。プロキシトークンは常に1つの場所にのみ存在し（available_proxiesまたはleased_proxies）、宣言された遷移のみがそれを移動できます。リソースのライフサイクル（利用可能 → リース済み → クールダウン中 → 利用可能）はネット自体の形状であり、事実上のステートマシンです。また、ネットのクールなアニメーションも提供されます。 フルサイズ — ウェブスクレイパーCPN、アニメーション 個人的には、この状態と遷移の統合には強気です。データベースは通常、これのデータ+型側と、チェック制約のような述語ツールしか扱いません。既存のシステムが状態関連の不変条件をアプリケーションコード、単体テスト、データベース制約（それぞれ個別の検証）に分散させているのに対し、CPNはこれらの懸念を一元化し、それらを使用してアプリの機能を定義します。新しいドメインとして、これらのシステムからどのような種類のバグが発生する可能性があるか、またはどのような種類の操作とパフォーマンスのトレードオフが必要かについて、多くの学習が ahead です。型システムは「無料ではない」ことで有名です。しかし、私はそれとともにさらに大きな機会があると考えています。 ---