# Part 7　健全性と正規化、そして「わざと unsound」 Source: https://rigor.typedduck.fail/ja/chibirigor/seasoned/part7-soundness/ > **Tip** > > 参考書（任意）：『TAPL』8章「型付き算術式」§8.3（安全性＝進行＋保存）、12章「正規化」、『しくみ』おわりに。 > 型理論の中心定理を据え、*なぜchibirigorはわざと健全でないのか*を形式の言葉で言い切る章です。 この章のゴール：「型システムとは何か」「健全とは何か」を定義し、chibirigor（とRigor）が**意図的に**その健全性を手放していることの意味を言葉にする。 Part 6では、フローを支える本物の**FactStore**（6種の事実、無効化、クロージャ捕獲）まで道具を作り切りました。最後に一段引いて、ここまで作ってきたものが「型システム」として何を保証し、何を*わざと*保証しないのかを、理論の言葉で言い切ります。 --- ## 7-1. 「型システム」の狭義と広義 『しくみ』おわりにの整理を借ります： - **狭義**：型システム＝**型付け規則**の集まり（どの式にどう型を付けるか） - **広義**：それに加えて、規則について*証明できる定理*、とくに**型安全性（健全性）**と**正規化可能性** **型チェッカー**は、「入力プログラムが型付け規則で説明できるか」を機械的に判定するプログラムです。前編で作ったものは、まさにこの「規則を機械的に決定可能にしたプログラム」でした。『TAPL』9章Figure 9-1の変数規則T-Varを、前編の`type_of`の`LocalVariableRead`節と並べると、規則とコードが一対一に対応しているのが見えます。 --- ## 7-2. 健全性（進行と保存） **型安全性（type safety / soundness）**の標準的な定式化は、2つの定理の組です（『TAPL』8.3）： - **進行（progress）**：型の付いた項は、値であるか、*次の評価ステップが必ず存在する*（＝行き詰まらない＝未定義動作に陥らない） - **保存（preservation / subject reduction）**：型の付いた項を1ステップ評価しても、*型は保たれる* 二つ合わせると：「**型の付いたプログラムは、評価のどの時点でも行き詰まらない**」。これが「型が付けば未定義動作に陥らない」という保証の中身です。「**Well-typed programs cannot go wrong**」（Milner）。 --- ## 7-3. 正規化（型が付けば止まる） もう一つの定理が**正規化可能性（normalization）**（『TAPL』12章）です。単純型付きラムダ計算では、**型の付いたすべての項は、必ず停止する**。`(λx. x x)(λx. x x)`（発散項 Ω）のようなものは、型が付きません。 鍵は自己適用`x x`です。`x`を「`x`を受け取る関数」と「その引数」の両方に使うには、`x : A -> B`かつ`x : A`、つまり`A = A -> B`という*再帰的な*型が要ります。単純型にはそれが無いので、Ω は型付け不能です。だから「型が付けば止まる」が破れません（再帰型を足すと話が変わる、後編Part 4）。 正規化（型が付けば必ず止まる）は単純型付きの中核の性質で、『TAPL』12章の主題です。再帰型（『しくみ』8章）や一般再帰を足すと一般には成り立ちません。そして**chibirigorは、この性質を持ちません**。相手は停止しない実Rubyだからです。 --- ## 7-4. なぜchibirigorはわざとunsoundなのか ここが、後編で最も大事な一節です。前編で作ったものは**健全ではありません**。わざとです。 健全なチェッカーは「型が付く ⇒ 絶対に安全」を保証する代わりに、**安全だが証明できないプログラムを弾きます**（保守側の誤検知）。動的言語の現実のコードは、その「安全だが証明しにくい」塊です。ここで健全性を貫くと、**動くコードが真っ赤**になる。だからchibirigor（とRigor）は、健全性を**意図的に手放し**ます。 **前編Part 9 §9-2で標語として挙げた「わざと見逃す4箇所」を、ここで §7-2の言葉（進行と保存）で言い直します**。 健全な型システムは「型が付く ⇒ 実行が行き詰まらない（progress）」を保証します。chibirigorの4つの穴は、いずれもこの**progress保証を*わざと*手放す**箇所です。つまり「型が付いても、`NoMethodError`等で*行き詰まり得る*」を許します。各穴が許してしまう「行き詰まり（stuck state）」はこうです： | 前編 §9-2の標語 | progress、preservationの言葉 | 許す「行き詰まり」 | |---|---|---| | ① `untyped`は何でも受理 | progressを放棄（`untyped`をどの期待型にも受理＝subsumptionを素通し） | `untyped`値が応えないメソッドを呼ぶ → `NoMethodError` | | ② openなhash、未知キー→`nil` | progressを放棄（幅部分型を引数で緩める） | 実は無いキーが`nil` → `nil`への呼び出しで停止 | | ③ `:maybe`を罰しない | progressを放棄（証明不能を`:no`に昇格させない） | `:maybe`が実は不一致 → 実行時の型エラー | | ④ 保守的ナローイング | progressの*検出*を放棄（disjoint、`Dynamic`を絞らない） | 絞れず見逃した枝の実エラーを報告しない | preservation（評価で型が保たれる）の側は、chibirigorはそもそも*強く主張しません*。怪しくなれば`untyped`にwidenするので、preservationはconsistency（`~`）の意味で自明に保たれます（型が合わなくなったら`untyped`に倒すだけ）。**手放しているのは主にprogress**、というのがこの4箇所の正体です。 形式的に言えば：**chibirigorは健全性（soundness）、とくにprogressを、誤検知の少なさ（"never frighten working code"）と引き換えに、限定的に放棄している**。これは欠陥ではなく**設計の選択**です。健全性は「バグを1つも見逃さない」を意味しますが、その代償（動くコードを脅かす）の方が、実用チェッカーでは高くつくと判断しているのです。 > **重要** > > **巻のブックエンド**：前編 §1-3で「動くコードを脅かさない／わからない所はそっと通す」と*前振り*した約束を、後編はここでprogress、preservationの言葉で*回収*しました。 > 双方向の地図を広げた後編Part 1（入口）と、健全性を「わざと手放す」設計を言い切るこの章とが、呼応します。 --- ## 7-5. gradualの2つの規律（consistencyとguarantee） 「では完全に何でもありか」というと、そうではありません。健全性は手放しても、gradual typingには**別の規律**があります。chibirigorが守っているのは、次の2つです。 ### 規律その1（gradual consistency `~`、型の側の規律） `untyped`（`Dynamic`）が絡むと、部分型`<:`は**両方向に通る**特別な関係になります。これを**gradual consistency（漸進的整合性）** `~`と呼びます（後編Part 2 §2-5から送られてくる論点）： - `untyped ~ T`も`T ~ untyped`も成り立つ（**対称**） - でも`~`は**推移的でない**：`Integer ~ untyped`かつ`untyped ~ String`でも`Integer ~ String`ではない - だから`untyped`を「何にでも化ける抜け穴」にしつつ、`Integer`と`String`の取り違えは依然`:no`にできる > **Note** > > `~`はgradual typingの学術慣例（Siek）の記号です。 > 実Rigorはドキュメントで記号衝突を避け、この関係を`consistent(A, B)`と綴ります（`~T`は否定、補型に予約）。 > 意味（対称、非推移）は同じです。 前編の三値`accepts`は、まさにこの`<:`（証明できる、できない）と`~`（untypedが絡む）を**一つの判定に畳む**ためのものでした： | 状況 | 結果 | |---|---| | `S <: T`が証明できる | `:yes` | | `untyped`が絡む（`~`だが`<:`は不明） | `:maybe` | | `S`と`T`が確実に互いに無関係 | `:no` | `~`が**非推移**だからこそ、`untyped`は無制限の抜け穴になりきらない。ここが「無秩序ではない」の一つ目の意味です。 ### 規律その2（gradual guarantee、注釈量の側の規律） もう一つが**gradual guarantee**（Siekら）です。型の側ではなく、*注釈の量と挙動の関係*に対する規律です： > **Note** > > 注釈を**増やしても減らしても**、プログラムの意味（通る、通らない、動作）は*連続的に*変わる。 > 型注釈を減らせばチェックは緩くなるだけで、急に壊れたりはしない。 chibirigorの「`untyped`に倒す」「注釈の無い所は照合位置を作らない」という設計は、このgradual guaranteeの素朴な現れです。注釈を1つ足したからといって、無関係な箇所が突然真っ赤になったりしない。**健全性は手放したが、無秩序ではない**の二つ目の意味です。 `~`（型の整合）とguarantee（注釈量への連続性）。この**2つの規律**が、「わざとunsound」を無秩序から区別しています。 > **Tip** > > **参考書メモ**：静的な`<:`までが『TAPL』15、16章の世界です。 > `untyped`を足した`~`は『TAPL』の*先*、gradual typing（Siek & Taha 2006）の領域で、前編Part 9、この章で扱う「わざとunsound」の核です。 > **Note** > > **`assert:`ディレクティブで「確かめた上で約束する」** > > Rigorがunsoundであっても、特定の箇所だけ健全性を取り戻す抜け道が**`assert`ディレクティブ**（RBSの拡張アノテーション）です。 > 検査、正規化を行うメソッドに付けます： > ```ruby # RBS側に書く（`.rb`本体にはインラインで書けない） # %a{rigor:v1:assert x is non-empty-string} def ensure_present!(x) = (raise if x.nil? || x.empty?) ``` > > 意味は「**このメソッドが返った後、*呼び出し元*の`x`は`non-empty-string`だ**」。 > 本体内ではなく*呼ぶ側*のスコープに事実を足す**ゲート**です。 > 推論が型を追えない動的ディスパッチや`eval`の後でも、ガードメソッドを一度通せば「ここから先は私が保証する」と宣言できます。 > 嘘を書けばその先の診断が嘘になります（`accepts`が`:yes`に化ける）。 > > | 機構 | 型の根拠 | > |---|---| > | `is_a?(String)` | Rigorが推論した事実 | > | `%a{rigor:v1:param: x is String}` | 宣言 → 呼び出し地点の照合＋本体での束縛 | > | `%a{rigor:v1:assert x is String}` | ガード通過後、*呼び出し元*の`x`を強制 | > > TypeScriptの*ユーザー定義型ガード*（`x is T`を返す述語関数）に近い役割です。 > Rigorでは「unsoundな型キャスト」ではなく「確かめた上で事実を足す操作」として扱います。 --- ## 7-6. 停止性をどう工学で守るか（余帰納、fuel、予算） 正規化（型が付けば止まる）もchibirigorは持てません。理論が「型が付けば止まる」を*証明*で保証するのに対し、実用チェッカーは「**解析そのものが止まる**」を*工学*で守ります。この章まで出てきた停止性の道具は、同じ対比の**相似形**が三段の大きさで並んでいます。 ### 余帰納（後編Part 4） 同値再帰の型等価判定は、放っておくと止まりません（`μX.{foo:X}`を展開し続ける）。後編Part 4は**余帰納（coinduction）＝仮定集合`seen`**でこれを断ちました。「いま比較中のペアを再び問われたら、等しいと*仮定して*打ち切る」。これは**正しく止める**解です（最大不動点としての部分型、『TAPL』21章）。 ### HKT還元fuel（後編Part 4、ADR-20） Rigorは再帰型を μ＋余帰納で直接は実装せず、軽量HKT（`Type::App`）＋**fuel（燃料）予算**で別解にしています（後編Part 4 §4-5から送られてくる論点）。高階型を展開するたびにカウンタを消費し、上限（既定64ステップ）で打ち切ります。これは**危なくなったら止める**解です。fuelが尽きれば結果を`:maybe`に倒し、`untyped`に逃がして安全側に着地します。 | 止め方 | 性格 | どこで | |---|---|---| | 余帰納（`seen`） | 正しく止める（最大不動点） | 教える等価判定（後編Part 4） | | HKT還元fuel（ADR-20） | 危なくなったら止める | Rigor実装済み | | 推論予算（ADR-41） | 危なくなったら止める（広義） | 設計済み、未実装 | ### 推論予算（inference budget、ADR-41） fuelがHKT還元という*局所*の停止を守るのに対し、より広義の**推論予算**（inference budget、ADR-41）も設計されています。解析全体を予算で打ち切る、fuelの大きな相似形です。ただしこちらは*現時点では未実装*（ADR-41はStatus: Proposed）です。 「型システムが正規化を保証する」という*理論の美しさ*が、実用チェッカーでは「**解析を予算で打ち切る**」という*工学*に置き換わる。余帰納（正しく止める）、fuel、予算（危なくなったら止める）は、同じ「展開をどう止めるか」という問いに対する、規模を変えた同じ答えです。実用チェッカーが「危なくなったら止める」を選べるのは、「分からなくなったら`untyped`に倒す」というgradualの割り切りがあるからでした。 --- ## 7-7. まとめ - 型システム＝狭義（型付け規則）＋広義（健全性、正規化の定理） - チェッカー＝規則の決定手続き - **健全性（進行と保存）**：型の付いたプログラムは評価のどの時点でも行き詰まらない（『TAPL』8.3） - **正規化**：型が付けば停止（『TAPL』12） - 再帰型や一般再帰を入れると一般には成り立たない - **chibirigorはわざとunsound**：健全性（とくにprogress）を「誤検知の少なさ」と引き換えに限定放棄 - 前編 §9-2の「見逃す4箇所」がその穴の正体 - §1-3の前振りをここで回収する - ただし無秩序ではない。**gradualの2つの規律**：consistency `~`（対称、非推移）とgradual guarantee（注釈量に対して挙動が連続）を守る - 正規化の代わりに、停止性を**工学**で守る - 余帰納（正しく止める）、HKT fuel（ADR-20、実装済み）、推論予算（ADR-41、設計済み、未実装）の、規模を変えた相似形 ## 演習 1. **穴をprogressで言い直す**：§7-4の表の4つから1つ選び、その穴が許す具体的な*動くRubyと、それが行き詰まる入力*を1組作れ（例：`untyped`受理 → `x.foo`が`NoMethodError`）。 2. **進行と保存**：「型が付いても`NoMethodError`になり得る」は進行と保存のどちらの放棄か。 chibirigorが保存はほぼ保てる理由（`untyped`へのwiden）と併せて述べよ。 3. **Ω が型付け不能**：`(λx. x x)`に単純型を付けようとして詰まる所（`A = A -> B`が要る）を示し、再帰型（後編Part 4）を足すと何が変わるかを一言で。 4. **2つの規律**：gradual consistency `~`が*非推移*であることと、gradual guaranteeが*注釈量*に効くことを、それぞれ「もしこの規律が無かったら何が壊れるか」で1文ずつ説明せよ。 5. **止め方を並べる**：余帰納（`seen`）、HKT fuel、推論予算の3つを「正しく止める、危なくなったら止める」で分類し、Rigorが後者を選べる理由（gradualの割り切り）を一言で述べよ。 **次章（Part 8、最終章）**：chibirigorの最小版から、本物のRigorの作り込み（プラグイン、キャッシュ、LSP、性能、baseline）へ橋を架けて、後編を締めます。