コンテンツにスキップ
Rigor

Matsumoto & Minamide 2008 (多相レコード型 Ruby 型推論) — Rigor 観点考察

Date: 2026-05-18.

Status: research note, no design commitments.

種別: 外部文献のRigor観点レビュー。

対象論文

Section titled “対象論文”

1. 論文要旨（一段落）

Section titled “1. 論文要旨（一段落）”

MLの型システムにGarrigueのカインド付き多相レコード型(maskable fields 付き)を載せて、Rubyプログラムの型推論ツールを設計・実装した。オブジェクト 型はα :: (L, U, R) ▷ αの三つ組カインドで表現し、Lは要求メソッド 集合、Uは定義メソッド集合、Rはメソッド名→関数型の関係述語。 インスタンス変数はTofteの命令的型変数（_β）で扱い、多相性を抑制 して副作用との健全性を保つ。組込みクラスは独自のシグネチャ言語 （def m :: C → C'）で記述し、Rubyのクラス再オープン文化に合わせて シグネチャとRuby実装が同一クラスに共存する型システムを設計。 負の位置（引数）はシグネチャのみから、正の位置（返り値）はシグネチャ

  • Ruby定義の両方から型を構築する非対称設計を採用。多相再帰 （Array/String/Integerの相互再帰）とmapのような正則でない多相 メソッドはクラス定義の有限回展開（複製）で近似する。実装はOCaml + 改造NodeDump、Ruby 1.8.5サンプル39本中21本を型推論可能 （list.rb：80行で1.26秒、ただし束縛型変数数57,479個）。健全性は 「Rubyのごく制限されたサブセットでのみ成立する」設計と明言。

2. Rigorの今の設計との対応関係

Section titled “2. Rigorの今の設計との対応関係”
論文側の概念Rigor側の対応物一致度・所見
シグネチャ言語def m :: C → C'RBS（およびそのRigor上位互換）本論文はRBS標準化（2020年頃）の12年前。事実上のRBS前史。同じく “Rubyプログラム本体に型は書かない／シグネチャを別途与える” という分離戦略は同じだが、RBSは.rbsファイル分離、本論文は同一クラスへの共存という構文上の違い。
多相レコード型 + GarrigueカインドRBSの公称型 + interface部分構造ハイブリッドRigorは公称型優位。多相レコード型の構造的アプローチは取らない。論文が苦しんだ「型表記が肥大化する／57k型変数」問題は、RBSが公称名を前面に出すことで概ね回避できている。これはSteep時代に同著者がたどり着いた工学的結論と整合。
命令的型変数（IVarの多相制限）Rigorのper-class IVar shape + initialization tracking（仕様はinternal-spec）問題領域は完全に同じ：副作用持つivarを多相に汚染させない。論文はTofte流の型変数分類、Rigorはper-class shapeの固定化＋カインド分離なしの実装で対処。論文の解は理論的に綺麗、Rigorの解は実用的に十分、というトレードオフの違い。
正の位置／負の位置の非対称扱いADR-5ロバストネス原則これは興味深い正味同方向の非対称性。論文「呼び出し側に課す要求（負位置）は少なめ、提供側として認める実装（正位置）は寛大に」。Rigor「引数（負位置）は寛容、返り値（正位置）は厳格」。呼ぶ側に楽をさせる側は両者一致、返り値側の厳格／寛容の向きが逆だが、これは「型推論ツールとして引っかかりを減らしたい（論文）」vs「型カタログとして信頼を作りたい（Rigor）」という目的差から自然に出てくる差。Rigorがロバストネス原則を選んだ正当化材料として、本論文の対義設計と比較するメモはADR-5に追記する価値がある。
多相再帰の “クラス展開” 対応RBSの宣言済み公称型 + 個別ジェネリクス論文ではArray/String/Integerの相互再帰が単相に潰れ、誤検出を生むためArray#0/Array#1のように手で展開。Rigor側はそもそもRBSがclass Array[Elem]を最初から多相で宣言できるので構造的な単相崩壊が起きない。Rigorが「手書きRBS（および将来sig-gen）を信頼する」（ADR-14, AGENTS.md § RBS Authorship）と決めている理由の傍証。
mapの正則でない型（多相再帰 + 多相メソッド）RBSのdef map: [U] () { (Elem) -> U } -> Array[U]論文は表現不能で「結果配列の要素型 = 入力配列の要素型」と保守的に近似 → 実用例`[1,2,3].map{
異種混合コレクションRigorのUnion型（value-lattice.md）論文は要素型を「共通フィールドのみ持つ構造型」で扱う（フィールドアクセス可、識別不可）。RigorはUnion（識別可、絞り込み必要）。Unionの方がnarrowing/refinementと相性が良い、Garrigue流の方がアクセスの自由度が高い、というのが本質的な差。Rigorがcontrol-flow narrowingを重視する設計なのでUnion寄りで正解。
as(Integer)キャスト案 (§7)RBS::Extendedの%a{rigor:v1:assert_type ...} / %a{rigor:v1:return_override ...} (rbs-extended.md)同方向の発想が12年の隔たりを超えて再合流している。論文の「asメソッドはランタイムでは何もしない・型推論側にだけ意味を持つ」設計は、Rigorのpredicate / assertion annotationと完全に同じ哲学。
健全性に対するスタンスRigorの “RFC 2119仕様＋実装は実用優先”完全一致。論文「実用的なRubyプログラムへの対応を理論的正当性より優先」。Rigor「robustness principleを採用、機械化された健全性証明は持たない」（ADR-5, implementation-expectations.md）。同著者の2010年CFA論文（姉妹ノート）でだけ証明を与えていたのは、対象をSemiRubyに絞れたからこそ。
varargsを扱えないRBSの*args: T / **kwargs: Tネイティブサポート論文ではprintを手でprint1/print2/print3に分割していた。RBS言語の表現力が何を解決したのかが具体的に見える例。
エラー出力が内部表現の生dump（§7課題）Rigorのdiagnostic policy / family hierarchy (diagnostic-policy.md, ADR-8)同著者がこの問題を早期から認識していたことが分かる。Steep〜Rigorの長年の投資が診断UXに集中している直接の系譜。
クラス継承の “親メソッドのコピー” 実装Rigor / RBSのlookupチェーン論文の実装単純化のための妥協。RigorはRubyの真の継承探索を保ったまま解析を回せる（identity維持）。

3. 論文がRigorに示唆する具体ポイント

Section titled “3. 論文がRigorに示唆する具体ポイント”

  1. 「型変数が万単位に爆発する」現象の証拠として、本論文のlist.rb 結果（束縛型変数57,479個）は引用価値が高い。Rigorが構造的多相 レコードを採用しなかった選択の正当化材料として、 ADR-1もしくはADR-3 に脚注を入れられる。

  2. ADR-5ロバストネス原則の対照例として、本論文の「負位置は シグネチャのみ・正位置は実装も含める」設計は、同じ “非対称性を 入れる” という方針の別解である。Rigorが選んだ方向と論文の方向の 対比を、ADR-5または docs/type-specification/robustness-principle.md の “Why this asymmetry, not the other” 節として整理する余地がある。

  3. as(klass)キャストとRigorの%a{rigor:v1:assert_type}の系譜的 近さは、RigorのRBS-extendedアノテーション設計の正当化材料。 同じ著者が12年隔てて同じ結論に達している事実は、設計選択の頑健性を 示す。

  4. 多相再帰の手動展開アプローチはRigorのsig-gen （ADR-14）のスコープ判断に示唆を 与える：完全自動な多相再帰解析を狙うのではなく、公称ジェネリクス の宣言コストを開発者に払ってもらう代わりに、推論側はその宣言を絶対視 するというRigorの戦略は、本論文が機械的な解として持ち込んだ 「クラス複製展開」を人間（ライブラリ作者）に肩代わりさせている 構造として理解できる。

  5. 健全性証明の戦略的不在が、同著者の2008 → 2010 → Steep → 現在 という流れの中で一貫した工学的判断であることを本論文が裏付ける。 Rigorが同じ判断を継承しているのは正統な路線にあり、独自に弁護する 必要はない。

  6. Steepへの系譜の起点として、本論文 → CFA論文 → Steep → RBSと いう流れの第一段がここにある。RBSの表現力(公称ジェネリクス・ varargs・block引数・多相メソッド)は、すべて本論文がML+カインド では表現できなくて困った場所に対応している。RBSの設計理由を 読み解くための「失敗ケース集」として価値が高い。

4. まとめ

Section titled “4. まとめ”

論文は、RubyをML流の構造的多相レコード型で型付けする試みが、 多相再帰・多相メソッド・varargs・健全性・型表記サイズという五つの壁 に同時にぶつかることを実証的に示した。Rigorは同じ著者の系譜の延長線上 にあるが、これらの壁をRBSという別の選択肢 (公称型優位 + 宣言主義

  • pluginによる拡張 + 部分構造のinterface)で迂回している。本論文は、 RigorがなぜGarrigue風の構造的型推論を採らないか・なぜRBS互換を 最優先するか・なぜ完全健全性を狙わないかという設計判断の歴史的な 妥当性検証として読める一級の資料である。特にADR-1, ADR-5, ADR-14,そしてRBS-extended アノテーション仕様の背景文献として明示引用するのに最適。

関連ADR / 仕様

Section titled “関連ADR / 仕様”

姉妹ノート

Section titled “姉妹ノート”

© 2026 TypedDuck. Licensed under CC BY-SA 4.0.