双方向型検査

型検査を、型を与えられて検証する「検査(checking)」と、式から型を割り出す「合成(synthesis)」の2モードに分けて規則を設計する手法。Γ ⊢ e ⇐ A（A をチェック）と Γ ⊢ e ⇒ A（A を合成）の2判断を使い分ける。

なぜ分けるのか

完全な型推論（Hindley–Milner）は、依存型・部分型・高ランク多相といった表現力の高い体系では決定不能・困難になる。双方向型検査は「要所に型注釈を要求する」代わりに、これらの体系でも実装しやすく・エラーが局所的になる。注釈の置き場所も原理的に決まる。

規則の向き

• 変数は環境から型を合成できる。適用 f x は f の型を合成し引数を検査する
• λ抽象は単独では型が決まらず検査向き（期待される関数型が要る）
• 注釈 (e : A) が 合成⇄検査の切替点。subsumption（合成した型を検査に流用）で両モードを接続

導出規則の例

判断は2本：Γ ⊢ e ⇐ A（A は入力＝検査）と Γ ⊢ e ⇒ A（A は出力＝合成）。各規則は「前提 ⟹ 結論」で読む。

例1: 関数の導入（検査）と適用（合成）

• λx.e は期待型 A → B を与えられて初めて引数 x の型 A が決まる → 検査向き。
• f x は f の型 A → B を合成し、そこから B を取り出し、引数を A で検査する → 合成向き。出力 B は前提から流れ出す。

例2: 切替点（注釈と subsumption）

• sub：合成した型 A が期待型 B と一致（部分型なら A <: B）なら検査が通る。合成→検査の橋。
• anno：注釈 (e : A) は検査モード（e ⇐ A）に降り、全体としては A を合成する。検査→合成の橋。
• この2規則が両モードを縫合する唯一の接点なので、「どこに注釈が要るか」が原理的に決まる：合成できない式（裸の λ、空リスト等）が合成位置に来たときだけ。

採用例

依存型言語のコア（Agda / Idris / Lean）、TypeScript の contextual typing、多くのモダン型検査器。出典は Pierce & Turner “Local Type Inference” (2000)、Dunfield & Krishnaswami のチュートリアル “Bidirectional Typing” (2021)。

押さえどころ（カード化候補）

• 双方向型検査とは → 型検査を「型を与えて検証する check (⇐)」と「式から型を割り出す synth (⇒)」の2判断に分け、規則ごとに向きを決める手法。
• なぜ分けるか → 完全推論 (Hindley–Milner) が困難な依存型・部分型・高ランク多相でも実装可能になり、エラーが局所的・注釈位置が原理的に定まる。
• 向きの割り当て → 導入規則 (λ・コンストラクタ・if枝) は check、除去規則 (変数・適用・注釈) は synth。出力 A が前提から流れ出すのが synth。
• 2モードの接合 → sub（合成型→検査へ）と anno (e:A)（検査→合成へ）の2規則だけが切替点。これにより注釈は合成不能な式が合成位置に来たときだけ要る。
• 採用先 → Agda/Idris/Lean のコア、TypeScript の contextual typing。出典は Pierce&Turner 2000、Dunfield&Krishnaswami 2021。

関連

• 推論規則 — 双方向化は推論規則を check/synth の2判断に割る設計
• TAPL — 型システム実装の土台。双方向はその実装技法
• 依存型 — 完全推論が困難な体系で双方向が要る代表
• 篩型 — 同じく注釈＋検査で扱う体系