コンテンツにスキップ
Rigor

Part 4　再帰型：μ と余帰納

参考書（任意）：『TAPL』20章「再帰型」、21章「再帰型のメタ理論」、『しくみ』8章。 型が自分自身を参照する再帰型を扱い、Rigorの別解（HKTとAppとfuel）と対比します。

前のPart 3では、ジェネリクスと型代入（一つの型が別の型を引数に取る仕掛け）を見ました。この章で扱う再帰型は、型が自分自身を引数のように呼び込む構造です。

前編は配列やハッシュを有限の構造として扱いましたが、現実のデータには自分自身を含むものがあります。JSON、木、連結リスト、ストリームがその例です。これらの型は自分を参照します。

4-1. なぜ再帰型が要るか

Section titled “4-1. なぜ再帰型が要るか”

いちばん身近な例はJSONです。JSON.parseが返す値は次のように定義されます：

value = null | bool | number | string | Array[value] | Hash[String, value]

valueの定義の中にvalueが出てきます。前編の型キャリアでは、この「自分を含む型」を書けませんでした。木やリストも同じです：

# 連結リスト：nil か、[要素, 残りのリスト]
list = nil | [Integer, list]

これらを正しく型として持つには、再帰型が要ります。

4-2. μ 型　再帰を畳む記法

Section titled “4-2. μ 型　再帰を畳む記法”

再帰型の標準記法はμ（ミュー）型です。μX. Tは「Tの中のXをμX.T自身で置き換えた型」を表します。たとえばlistは：

μList. (nil | [Integer, List])

X（やList）は型変数で、「自分自身が入る穴」を指します。Part 3で見たジェネリクスの型変数とは役割が違い、ここでは「再帰で自分が入る位置」を表します。

展開（unfold）：μ 型は、変数に自分自身を代入して一段ほどくことができます。

μList.(nil | [Integer, List])
  =  nil | [Integer, μList.(nil | [Integer, List])]   （一段展開）
   畳んだ形                       一段展開した形
   ┌─────────────┐   unfold →    ┌──────────────────────────────┐
   │ μList.{ … List } │  ───────────  │ { … μList.{ … List } }          │
   └─────────────┘   ← fold       └──────────────────────────────┘
        （同じ型を指す。展開は無限に続けられる ― だから等価判定で止め方が要る）

図4-1　μ型の畳（fold）と展開（unfold）

▼ 図4-1　μ 型の畳（fold）と展開（unfold）。両者は同じ型。展開は際限なく続くので、等価判定には「止める仕掛け」（§4-4の余帰納）が要る。

畳んだ形と一段展開した形は同じ型を表します。しかしデータ構造としては別物です。この「畳と展開が等しい」をどう扱うかが、再帰型の実装の核です。

4-3. 同値再帰vs同型再帰

Section titled “4-3. 同値再帰vs同型再帰”

再帰型には2つの流儀があります（『TAPL』20.2）：

  • 同型再帰（iso-recursive）：畳む、展開する場所をユーザーが明示する（fold/unfold）
    • 実装は楽（等価判定で再帰を追わない）ですが、書く側が面倒です。
  • 同値再帰（equi-recursive）：畳んだ形と展開した形がそのまま等しい
    • 注釈不要で書きやすいですが、等価判定の実装が難しくなります（再帰を追う必要があります）。

TypeScriptも多くの実用言語も同値再帰を採り、『しくみ』8章もこちらを実装します。直感的だからです。ML系は同型再帰が多く、他機能との相性が理由です。

4-4. 等価判定の停止性と余帰納

Section titled “4-4. 等価判定の停止性と余帰納”

同値再帰の難所は、型の等価判定が止まらないことです。μX.{foo:X}とμY.{foo:Y}が等しいかを調べようとすると、Xを展開、Yを展開、fooの中を比べる、また元の比較に戻る、という無限ループになります。

解は余帰納（coinduction）＝仮定集合です。「いま比較中のペア」を集合seenに覚えておき、同じペアを再び問われたら「等しい」と仮定して打ち切ります。実際に動くRubyで書くとこうなります（型は基底＝Symbol、レコード＝Obj、μ＝Rec、型変数＝Var）：

# 畳んだ形と展開した形を等しいと見なす等価判定。
# seen は「いま比較中のペア」。同じペアを再び問われたら true と仮定して止める（余帰納）。
def type_eq(s, t, seen = [])
  return true if seen.any? { |s2, t2| naive_eq(s2, s) && naive_eq(t2, t) }
  return type_eq(unfold(s), t, seen + [[s, t]]) if s.is_a?(Rec)
  return type_eq(s, unfold(t), seen + [[s, t]]) if t.is_a?(Rec)


  case [s, t]
  in [Symbol, Symbol] then s == t
  in [Obj, Obj]
    s.fields.size == t.fields.size &&
      s.fields.all? { |k, v| t.fields.key?(k) && type_eq(v, t.fields[k], seen) }
  else false
  end
end

seenの判定に使うnaive_eqは、束縛変数名の違いだけを吸収する α 同値（展開しない）です。μX.{foo:X}とμY.{foo:Y}を「同じ」と見なすために、名前の対応表mapを引き回します。これはPart 3のジェネリクスで出た α 同値（「根は一つ」＝束縛変数の名前は本質でない）と同じ技法です。

このnaive_eq、unfold、substを含む全体は、単体で走る設計スケッチexamples/mu_typeeq.rbにあり、ruby mu_typeeq.rbで次が緑になります：

PASS: muX{foo:X} == muY{foo:Y} (α + cycle)
PASS: muX{foo:X} == {foo: muX{foo:X}} (fold/unfold)
PASS: muX{foo:X} != muY{bar:Y} (field name)
PASS: stream fold == unfold (α)
PASS: Num == Num
PASS: Num != Bool

「証明しようとしているまさにそのことを、途中でまた問われたら、成り立つと認める」。これが余帰納の心です。『TAPL』21章がこのアルゴリズムと、その正しさ（最大不動点としての部分型）を展開します。

4-5. 発展ノート：Rigorの別解（HKTとfuel）

Section titled “4-5. 発展ノート：Rigorの別解（HKTとfuel）”

Rigorは、再帰型を μ と余帰納で直接は実装していません。代わりに軽量HKT（higher-kinded type）を使います（Type::App）。JSON.parseの戻りはApp[:"json::value", [String]]という不透明な高階型適用（key型を引数に取るarity 1）で、必要なときに登録済みの本体へ還元されます：

App[:"json::value", [String]]
  → Value = Literal | Array[Value] | Hash[String, Value]   （再帰 union へ還元）

ここで余帰納のseenに当たるのがfuel（燃料）予算です。「再帰の展開をどう止めるか」という同じ問題に、『しくみ』と『TAPL』は理論的に（余帰納で正しく等価判定）、Rigorは工学的に（fuelで安全に打ち切り）答えています。この「余帰納vs予算」という停止性の工学の総括は、健全性を扱う後編Part 7にまとめてあります（gradualの割り切りとあわせて読み解きます）。

4-6. chibirigor本編では作らなかった

Section titled “4-6. chibirigor本編では作らなかった”

前編は再帰型を非対象にしました（前編Part 6でHashShapeとTupleを有限のまま扱い、HKTとApp、fuelは不実装と宣言しています）。理由は複雑さ予算です。μ と余帰納もHKTとfuelも、最小版の主旨（双方向、gradual、フロー）から外れます。後編で概念として回収するのが正解でした。

もし最小実装を足すなら、型キャリアにRec(name, body)とTypeVar(name)を加え、acceptsと等価判定にseenを持つ形になります。これが μ と余帰納の最小形（『しくみ』8章のRuby移植）です。HKT版はURI参照とfuelで別実装になります。

4-7. まとめ

Section titled “4-7. まとめ”
論点要点
なぜ再帰型JSON、木、リスト、ストリームは、型が自分を参照する再帰型
μ 型再帰を畳み、展開で一段ほどく。畳と展開は同じ型
2つの流儀同値再帰（注釈不要、実装難）vs 同型再帰（注釈必要、実装易）。実用は同値再帰が主流
等価判定止まらない → 余帰納（seen仮定集合）で打ち切る（『TAPL』21章）
Rigorの別解HKTとAppとfuel（HKTの根拠は『TAPL』29章）：余帰納の代わりに燃料予算で打ち切る（停止性の工学の総括はPart 7）

演習

Section titled “演習”
  1. 畳と展開をトレース：μX.{foo:X}と{foo: μX.{foo:X}}（一段展開）が等しいことを、examples/mu_typeeq.rbのtype_eqに沿って手でたどれ（seenに入るペアを1つ書け）。
  2. なぜ止まるか：μX.{foo:X} == μY.{foo:Y}の判定で、seenを使わなかったら何が起きるかを述べ、seenが無限ループをどう断つかを1文で説明せよ。
  3. 理論vs工学：再帰の展開を止める方法として「余帰納（seen）」と「fuel予算」を比べ、なぜ実用チェッカー（Rigor）が後者を選べるのか（gradualの割り切り）を述べよ。

次章（Part 5）：前編の素朴な型推論を、Rigorの本物の型推論へ拡張します。呼び出し元から引数の型を埋め戻す単一化（unification）を扱い、ここでTypeProfとの対比を一本化します。

この章の設計スケッチ → examples/mu_typeeq.rb（ruby mu_typeeq.rbで自己チェック）

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