Appendix — The Liskov Substitution Principle

リスコフの置換原則（Liskov Substitution Principle、LSP） — ある型が別の型を置換するとは何を意味するかについての古典的な言明 — と、Rigorの設計とを橋渡しするページである。このページの主張は小さく、そして一度見えてしまえば見なかったことにしにくい:

Rigorのロバストネス原則（robustness principle、型のためのPostelの法則、戻り値に厳密でパラメータに寛容）は、反対方向から到達したLSPのシグネチャ規則そのものである。LSPは、より広いパラメータ / より狭い戻り値という非対称性を、「置換可能性は正しさを保たねばならない」からトップダウンに導く。Rigorは同一の非対称性を、「呼び出しサイトの摩擦を最小化し、下流の精度を最大化して、Rubyプログラマーが実際に型チェッカーを走らせるようにする」からボトムアップに導く。2つの動機、1つの規則である。

この収束が重要なのは、Rubyプログラマーがどんな型チェッカーに対しても当然抱く心配 — こいつは私のイディオムと喧嘩するのか？ — に答えるからである。ここでの答えはノーだ: Rigorが静かに適用する規律は、RubyコミュニティがすでにSOLIDの「L」として教えている規律と同じであり、慎重なダックタイパー（duck typer）が本能的に従っているのと同じものである。

頭字語についての注。このリポジトリのそれ以外のすべての場所では「LSP」は言語サーバープロトコル（Language Server Protocol）を意味する（ADR-19、rigor lsp）。このページ、そしてこのページに限ってのみ、「LSP」はリスコフの置換原則を意味する。この衝突は不幸なことに完全に慣習的なものである。コーパスの残りは言語サーバーの意味を保つ。

このページは記述的であって規範的ではない。ここでの記述が型仕様と食い違う場合は、仕様が拘束する。

この付録の内容 5秒で分かる要点 · LSPが実際に述べていること · LSPは振る舞いに関するもの · シグネチャ規則 = ロバストネス原則 · 分散とシグネチャ規則 · 事前条件（反変パラメータ） · 事後条件（共変戻り値） · 不変条件と履歴制約 · 振る舞い的vs名前的部分型 · RubyがLSP違反を許す場所 · クロス階層のオーバーライド互換性 · Rigorがチェックしないこと · 読書リスト

5秒で分かる要点

LSPの義務	それをすでに尊重しているRubyのイディオム	Rigorのサーフェス（surface）
部分型（subtype）は、上位型が期待されるどこででも置換してよい	ダックタイピング（duck typing） — 「私が送るメッセージに応答するなら、それを使える」	名前的型優先＋構造的ファセット＋ケイパビリティロール（capability role）
シグネチャ規則（signature rule） — パラメータは反変（contravariant）、戻り値は共変（covariant）	「使える限り最も広いものを受け入れよ。約束できる限り最も具体的なものを返せ」	ロバストネス原則（ADR-5） — 寛容なパラメータ（第2句）、厳密な戻り値（第1句）
部分型で事前条件（precondition）を強化してはならない	オーバーライド（override）は親が受け入れた入力を拒否すべきでない	第2句: パラメータは正しさを保つ最大のキャリア（carrier）へ広げられる
部分型で事後条件（postcondition）を弱化してはならない	オーバーライドは親が約束したものより具体性の低いものを返すべきでない	第1句: 戻り値は正しさを保つ最小のキャリアへ絞り込まれる。`def.return-type-mismatch`
不変条件（invariant）は保たれねばならない。履歴制約（history constraint）	親の不変条件を壊す状態遷移を加えるな。`freeze`を尊重せよ	副作用効果モデル + ファクト安定性 + `frozen?`ナローイング（部分的。§「不変条件」参照）
例外互換性 — 驚くような新しい例外を出さない	契約が文書化しているものをrescueせよ	内部の例外/非局所脱出効果（オーバーライド間では未チェック。§「Rigorがチェックしないこと」参照）

LSPが実際に述べていること

Barbara Liskovの1987年OOPSLA基調講演（Data Abstraction and Hierarchy）はその直観を述べた:

ここで欲しいのは、次のような置換性質のようなものである: 型Sの各オブジェクトo1について、型Tのオブジェクトo2が存在し、Tの観点で定義されたすべてのプログラムPについて、o1をo2に置き換えたときにPの振る舞いが変わらないならば、SはTの部分型である。

Liskov & Wing 1994（A Behavioral Notion of Subtyping、ACM TOPLAS）がこれを厳密にした。振る舞い的部分型（behavioral subtyping）S <: Tは2群の条件を要求する:

シグネチャ規則

部分型が上位型と共有するすべてのメソッドについて:

反変なパラメータ — 部分型のメソッドは、上位型が受け入れたすべての引数型を少なくとも受け入れねばならない（より多く受け入れてもよい）。
共変な戻り値 — 部分型のメソッドは、上位型の戻り値型を高々返さねばならない（より具体的なものを返してもよい）。
例外規則 — 部分型のメソッドは、上位型のものより少ない例外型を送出してよく、新しいものは決して送出しない。

振る舞い（メソッド）規則

シグネチャを超えて、振る舞いが互換でなければならない — これがシグネチャのみの型チェッカーの大半がエンコードしない部分である:

事前条件を強化してはならない。部分型のメソッドは、呼び出し元に対して上位型のものより多くを要求してはならない。
事後条件を弱化してはならない。部分型のメソッドは、上位型のものが保証したものを少なくとも保証せねばならない。
不変条件は保たれねばならない。すべての上位型インスタンスについて真である性質は、すべての部分型インスタンスについて真であり続ける。
履歴制約。部分型は、上位型の仕様がオブジェクトの生涯にわたって禁じている状態変化を許してはならない（例えば、可変なPointが不変なPointの部分型になることを排除する規則）。

振る舞い規則は、部分型付けの法則として述べられた契約による設計（Design by Contract）の継承規律である（Bertrand Meyer、Eiffel）: require句は階層を下るにつれ弱まり、ensure句は強まり、invariant句は累積する。

LSPは振る舞いに関するものであり、静的型に関するものではない

ときどき次のような主張が現れる: 「Rubyは動的型付けなので、LSPは厳密には適用されない静的型付けの規則だ。」これは原則を逆さまにとらえており、なぜそうなのかをはっきり言う価値がある。

LSPは型チェッカーについての規則ではない。それは置換のもとでの観測可能な振る舞いについての規則である — Liskov自身の枠組みは「Tの観点で定義されたすべてのプログラムP」を量化し、Sが代入されたときにそれらの振る舞いが変わらないことを求める。1994年の論文のタイトルは意図的だ: A Behavioral Notion of Subtyping。シグネチャ規則は型システムの形をした半分にすぎない。荷重を担う半分は振る舞い規則 — 事前条件、事後条件、不変条件、履歴 — であり、それらはコンパイラが何を受理するかではなく、コードが実行時に何をするかについての言明である。

その振る舞いへの焦点こそが、LSPをRubyのような言語により適用しやすくする — 適用しにくくするのではない:

名前的に型付けされた言語では、コンパイラがシグネチャの半分をあなたの代わりに強制するので、LSPは「型チェッカーがすでにやったこと」のように感じられる。興味深く、自動化されていない部分は振る舞いの半分である。
Rubyにはどちらの半分も強制するコンパイラがない — だから原則全体、シグネチャと振る舞いの両方が、プログラマーが担う規律である。Rubyにおける「部分型」はメッセージと振る舞いの置換可能性（ダックタイピング）によって定義され、それはまさにLSPが言明される対象の関係である。形式化が難しい言語こそ、振る舞いの置換可能性の規律が最も報われるケースだ — 静的なセーフティネットがないとき、それが唯一利用できるセーフティネットである。

だから「Rubyは静的型付けではない」は、LSPを真剣にとらえるための議論であって、それに反する議論ではない。LSPは、古典的な型システムがその形を完全には捉えられない言語において、置換の振る舞い的安全性について推論することを可能にするツールである。動作しているすべてのダックタイプのRubyプログラムは、すでにLSPの形をした何かが成り立つことに依存している — 呼び出し元は、受け取ったオブジェクトが、それが書かれた相手の契約と互換に振る舞うと仮定している。

これに対するRigorの関係

Rigorは、プログラムがLSPに従うという直接の静的保証を提供しない。振る舞い的部分型を証明せず、クロス階層のオーバーライド互換性をチェックせず、事前/事後条件の契約を検証しない（§「Rigorがチェックしないこと」）。この狭い読み方では、「RigorはLSPチェッカーではない」は真である。

しかしアイデアには相当な共通基盤があり、それがこの付録全体の要点である。Rigorの設計は、LSPが形式化するのと同じ振る舞いの置換可能性の本能に舵を切られている:

ロバストネス原則は、LSP的に正しいシグネチャの形（広いパラメータ、狭い戻り値）をデフォルトで推論する（次の§）。
ケイパビリティロールは、ダックタイピングがそうするのと同じやり方で — 名前的同一性ではなく振る舞い（応答するメッセージ）によって — 置換可能性をモデル化する。
副作用効果とファクト安定性のモデルは、状態変化が壊しえた性質を信頼し続けることを拒む — 局所的に適用された履歴制約の本能である。

したがってRigorは、LSPの振る舞い的世界観を共有し、Rubyにおいて静的に証明可能な部分を機械化するツールとして読むのが最良であり、残りはそれが常にそうであった規律として残す。原則とツールは、ツールが証明には至らない場合でも、精神において揃っている。

シグネチャ規則はRigorのロバストネス原則である

これがこのページの核心である。2つの規則を並べて置こう:

位置	LSPのシグネチャ規則	Rigorのロバストネス原則
パラメータ	反変 — 上位型と少なくとも同じだけ受け入れる	寛容（第2句） — 正しさを保つ最も広いキャリア
戻り値	共変 — 上位型が約束したものを高々返す	厳密（第1句） — 正しさを保つ最も狭いキャリア

これらは同じ非対称性である。異なるのは、各システムがなぜそれに手を伸ばすかである。

LSPの導出はトップダウン。「SはTが期待されるどこででも使えねばならない」から始める。Tに対して書かれた呼び出し元は任意のT型の引数を渡しうるので、Sのメソッドはそれらすべてを受け入れねばならない — パラメータは広がる方向にしか動けない。Tに対して書かれた呼び出し元は結果をTとして使うので、SのメソッドはあらゆるTコンテキストが消費できるものを返さねばならない — 戻り値は狭まる方向にしか動けない。非対称性は置換可能性からこぼれ落ちる。選ばれたものではない。

Rigorの導出はボトムアップ。ADR-5は、置換可能性の証明ではなくRuby採用の問題から始める（robustness-principle.md）:

過度に厳密なパラメータ型は、呼び出し元にすべての呼び出しサイトで防御的な型強制（x.to_s、x || ""、Array(x)）を貼り付けさせる。その回避策は荷重を担うようになり、意図を隠す。だからRigorはパラメータを「本体が実際に使えるあらゆるもの」 — ケイパビリティロール、構造的インターフェース、上位型 — へ広げる。
過度に広い戻り値型は、すべての下流の消費者が必要とする精度を捨てる。Array#sizeがnon-negative-intではなくIntegerと型付けされると、後続のあらゆるif size > 0が崩壊する。だからRigorは戻り値を「本体が証明可能に生み出す最も具体的なもの」へ絞り込む。

まったく異なる2つの出発点 — 1994年の置換可能性の定理と、2020年代の「Rubyプログラマーにそこら中で.to_sを書かせないでくれ」というエルゴノミクスの懸念 — が、同一の規則に着地する。その収束が安心材料である: Rigorの実用的でRubyファーストなデフォルトは、古典的なオブジェクト指向の型規律からの逸脱ではない。それを再導出しているのである。

# 第2句 / 反変なパラメーター: 本体は #upcase だけを使うので、
# パラメーターは名前的な String ではなく「upcase に応答する
# あらゆるもの」へ広がる。String だけを受け入れるオーバーライドは
# 事前条件を*強化*することになる — LSP違反であり、まさに第2句が
# 遠ざける過度に厳密な形である。
def shout(thing)
  thing.upcase
end

# 第1句 / 共変な戻り値: 本体は証明可能にレシーバを返すので、#dup は
# 広げられた Object ではなく `self`（Array[Integer]）を返す。
# Object を返すと事後条件を*弱化*することになる。
copy = [1, 2, 3].dup
assert_type("Array[Integer]", copy)

型理論の付録の漸進的保証（gradual guarantee）（§「ブレーム、漸進的保証、そして信頼境界」）との関連は直接的である: シグネチャ規則を構成によって尊重するシステムは、「アノテーションを追加しても以前にパスしていた呼び出しサイトを決して壊さない」も満たす。なぜなら、正しく広げられたパラメータと正しく狭められた戻り値こそ、置換可能性を保つアノテーションだからである。

分散とシグネチャ規則

シグネチャ規則は分散（variance）についての言明であり、RigorはRBSの分散の語彙を継承する（型理論の付録の§「分散」）:

共変（out T） — プロデューサー位置。シグネチャ規則の戻り値側。
反変（in T） — コンシューマー位置。シグネチャ規則のパラメータ側。
不変 — 両方を同時に。可変ストレージ。

Rubyの可変コンテナ（Array、Hash、Set）は要素型に対して不変であり、これがLSPと素朴な直観が衝突する典型的な場所である。Array[Integer]がArray[Numeric]を置換すべきだという「自明な」考えは、呼び出し元がarr.push(1.5)と書いた瞬間に不健全になる — 古典的な「共変な配列は壊れている」という戒めの物語（JavaのArrayStoreException）である。RBSはこれらのコンテナを不変と宣言する。Rigorはその宣言を尊重するので、不健全な置換を決して提供しない。シグネチャ規則は、変更を行うメソッド（pushは反変な位置で要素を取り、[]は共変な位置でそれを返す）に適用されると不変性を強制する — そしてRigorは、分散を再導出するのではなくRBSを信頼することで、これを無償で得る。

self型（self type）は、シグネチャ規則の共変な戻り値のケースを、オブジェクト指向のRubyにとって荷重を担う形にしたものである。RBSのselfキーワード（def dup: () -> self）は「私は自分自身のクラスを返す」を意味するので、部分型の継承したメソッドは部分型を返す — 共変な戻り値が自動的に尊重される。より深い扱いは§「F有界多相とselfType」を参照。LSPの読み方は単に、selfがSub#dupにSubを返させ続け、決して祖先へ広げ戻して事後条件を弱化させないための機構だ、ということである。

事前条件: 反変なパラメータとダックタイピング

振る舞い規則「事前条件を強化してはならない」は、Rubyにおいてはダックタイピングのほぼ言い換えである。Rubyのメソッドはどのクラスを望むかを宣言しない。どのメッセージを送るかを宣言する。それらのメッセージに応答するオブジェクトはどれも置換可能である — これはまさに「呼び出し元に必要以上を要求するな」である。

Rigorはこれをケイパビリティロールと構造的インターフェース（第2句の道具箱）でエンコードする:

本体が使うもの	過度に厳密（強化された事前条件）	第2句 / LSPに優しい
`#write`のみ	`IO`	`_Writable`（StringIO、Tempfile、モックすべてが適格）
`#upcase`のみ	`String`	`#upcase`を持つロール
`+`、`-`、`<=>`	`Integer`	`Numeric`
`#to_s`、nilガード付き	`String`	`String

# パラメーターを IO に*狭めた*部分型のオーバーライドは、事前条件を
# 強化して置換可能性を壊すことになる。Rigor が親に対して推論する
# パラメーターはすでに _Writable なので、LSP を尊重するオーバーライドは
# Rigor がデフォルトで推論するものと同じでもある。
def dump(stream)
  stream.write(serialize)
end

Dynamic[T] / respond_to?でナローイングされたレシーバーに対する開世界仮定（open-world assumption）（§「オープンワールド対クローズドワールド」）は、呼び出しサイトにおける同じ本能である: Rigorは動的な値の完全なメソッドセットを知っていると仮定しないので、実行時が決して要求しなかった事前条件（「ちょうどこのクラス」）を製造しない。事前条件を強化することは、動作しているダックタイプのコードに偽陽性を発火させることを意味する — それはプロジェクトの偽陽性の規律と真っ向から衝突する。LSPと「動作しているコードを決して怯えさせない」は同じ方向を指している。

事後条件: 共変な戻り値とself型

「事後条件を弱化してはならない」は第1句であり、それには具体的な強制サーフェスがある: def.return-type-mismatch（ADR-8）。メソッドが宣言されたRBS戻り値型を持ち、本体の推論された型がそれを満たせないとき、Rigorはエラーを出す:

class Repo
  # RBS:  def find: (Integer) -> User
  def find(id)
    @cache[id]   # 推論: User | nil
  end
  # def.return-type-mismatch — 本体は nil を返しうるので、宣言された
  # 「-> User」の事後条件を弱化する。
end

これは、ひとつのメソッドをそれ自身の宣言された契約に対して適用した事後条件規則である。スコープを正確に押さえておこう（次の節で効いてくる）: def.return-type-mismatchは、本体をそのメソッド自身のRBSシグネチャに対してチェックするのであって、上位クラスのシグネチャに対してではない。共変性を階層をまたいで検証するために部分型のオーバーライドを上位型の宣言された戻り値に対して比較する補完的なチェックは、v0.1.15でdef.override-*ルールファミリーとして出荷された（後述の§「クロス階層のオーバーライド互換性」）。ロバストネス原則は個別に著作された各シグネチャを正直に保つ。そしてオーバーライドファミリーが、著作された子の契約が著作された親の契約を置換することを検証する。

共変な戻り値の半分は、分散の節から鏡映して、ここでself型がその働きに見合う理由でもある: def dup: () -> selfは、部分型の継承したdupが部分型を返し続けることを保証する。部分型でdupの戻り値をObjectへ広げるシグネチャは事後条件を弱化することになる。selfはLSP的に正しい振る舞いを、表現可能な唯一の振る舞いにする。

不変条件と履歴制約

3番目と4番目の振る舞い規則 — 不変条件の保存と履歴制約 — は、Rigorのカバレッジが本当に部分的な場所であり、何がモデル化され何がされていないかを正確に述べる価値がある。

Rigorは、変更・非局所脱出・クロージャ脱出を追跡する内部の効果モデル（§「エフェクトシステム」）を持つ。不変条件に関係するユーザーに見える帰結:

変更はナローイングを無効化する（ファクト安定性）。ある変数についての絞り込まれたファクトは、変更を行う呼び出しのあと破棄される。なぜなら、その変更がナローイングの依拠する性質を壊したかもしれないからである。これは「不変条件はすべての操作を生き延びねばならない」の局所的な、メソッド内のアナログである — Rigorは、変更が偽にしえたファクトを信頼し続けることを拒む。
frozen?ナローイング。Rigorはfrozen?で絞り込む。frozenなオブジェクトとは状態履歴が閉じたものであり — Rubyが提供する履歴制約の最も強い形である。不変な値オブジェクト（Data.define、frozenなリテラル）は、履歴制約を構成によって満たすイディオムであり、Rigorはそれらを精密に型付けする。

Rigorがしないこと: それはクラス階層をまたいで、部分型の追加したメソッドが上位型の宣言された不変条件を保つことを検証せず、Liskov-Wingの履歴制約を部分型付けのチェックとして強制もしない（可変なPointが不変なPointの部分型になることを禁じる規則）。Rubyにはそのような不変条件を宣言するサーフェスがなく、それらを推論することはASTを歩く、偽陽性なしの包絡線の十分に外側にある。履歴制約の精神は運用的に尊重される（ファクト安定性、frozen?）が、部分型付けのチェックは実装されていない。

Rubyにおける振る舞い的部分型と名前的部分型

LSPは振る舞い的部分型についての言明だが、Rubyの実行時ディスパッチは名前的かつmixin的である: is_a?は祖先チェーンを参照し、Comparable / Enumerableは名前的なmixinを通じて届けられる振る舞い的な契約である（モジュールをincludeし、必要なメソッドを1つ実装し、残りを継承する）。したがってRubyは2つを混ぜ合わせる — 同一性のための名前的継承、共有された振る舞いのためのモジュールmixinである。

Rigorの名前的型優先＋構造的ファセットの立場（§「名前的型付け対構造的型付け」）はこれに正確に対応する:

名前的クラスはモデル化の単位であり、宣言された契約の安定した付着点である。
interface _Comparableスタイルの構造的シェイプとケイパビリティロールは、純粋な名前的部分型が取り逃す、振る舞い的でダックタイプの置換可能性を捉える。

Rubyコミュニティはすでに型理論なしでLSPを教えている。Sandi MetzのPractical Object-Oriented Design in Rubyは、SOLIDの「L」を次のように枠づける: サブクラスは上位クラスと置換可能であるべきだ、そして実践的なテストは、上位クラスに対して書かれた呼び出し元が変わらず動作し続けることである。これは平易なRubyで述べたLiskovの1987年の一文である。Rigorの貢献は、その規律のシグネチャの半分を機械チェック可能にすること — しかもプログラマーに一つのアノテーションも書かせずに、である。なぜならロバストネス原則がLSP的に正しいパラメータと戻り値の形を自動的に推論するからである。

RubyがLSP違反を許す場所 — そしてRigorがすること

Rubyはいかなる静的なオーバーライド規律も課さない。異なるアリティ（arity）、より狭いパラメータ、無関係な戻り値、まったく新しい例外でメソッドをオーバーライドでき、インタプリタは（実行時のパスが非互換にぶつかるまで、そしてぶつからない限り）文句を言わない。これらのどれもが潜在的なLSP違反である:

class Animal
  def speak(volume) = "..." * volume
end

class Mute < Animal
  def speak              # アリティを狭めた: 事前条件を強化
    raise NotImplementedError   # 新しい例外: 例外規則違反
  end
end

健全なチェッカーならそのオーバーライドをフラグするだろう。Rigorは、その偽陽性なしの立場により、すべてのオーバーライドに吠えない — なぜならRubyでは、形を変えてオーバーライドすることは意図的で正しいことがしばしばだからである（テンプレートメソッドの精緻化、method_missing、DSL駆動の再定義、define_method）。あらゆる形の変化をLSPエラーとして扱えば、膨大な量の動作しているコードを怯えさせることになる。

代わりにRigorは、契約が壊れていると証明できる場所でのみ発火する:

call.argument-type-mismatch — 呼び出しサイトが、宣言されたパラメータが受け入れられないものを証明可能に渡すとき。
def.return-type-mismatch — 本体が、それ自身の宣言された戻り値を証明可能に生み出せないとき。

どちらも著作された契約に対する局所的な証明であって、思弁的なクロス階層の置換可能性の判断ではない。これがLSP実用主義の立場である: 証明できる部分を強制し、著作するすべての場所でLSP的に正しい形を推論し、Rubyのイディオムが日常的かつ正当にぼかすオーバーライド互換性の問いについては沈黙を保つ。

より深い点: ロバストネス原則が広いパラメータと狭い戻り値をデフォルトで推論するので、最も一般的なLSP的に正しい設計は、Rigorのもとでは最小抵抗の道でもある。Rigorの推論する形に従うプログラマーは、意識せずに、事前条件を強化せず事後条件を弱化しないオーバーライドを書いている。Rigorは診断によって取り締まるのではなく、デフォルトを通じてLSP準拠へ向けてそっと後押しする。

クロス階層のオーバーライド互換性

v0.1.15以降（ADR-35）、Rigorはオーバーライドを、それが継承する契約に対して実際に比較する — プロジェクト定義のクラス/モジュール階層をまたいで適用されたシグネチャ規則である。def.override-*ファミリーは3つのルールから成る:

def.override-param-narrowed — パラメータの反変性: オーバーライドはパラメータ型を狭めて事前条件を強化してはならない。
def.override-return-widened — 戻り値の共変性: オーバーライドは戻り値型を広げて事後条件を弱化してはならない。
def.override-visibility-reduced — オーバーライドは継承した可視性を縮小してはならない（public → protected/private）。

このファミリーは、ロバストネス原則に対する荷重を担う規律の対応物である: 原則が推論されたシグネチャを置換可能性へ偏らせるのに対し、これらのルールは著作されたものを検証する。これらは偽陽性の規律のためにゲートされている — オーバーライドと影にされた祖先の両方が著作されたシグネチャ（手書き / rbs-inline / バンドルされたRBS。どちらかの側が推論のみなら沈黙を保つ）を持たねばならず、証明可能（:no）な違反でのみ発火し、重大度はseverity_profile:を通じてマップされる（lenient → off、balanced → warning、strict → error）。祖先のスコープは上位クラスチェーンに加えてinclude/prependされたモジュールであり、クロスファイルで解決される。

狭めに見える正当な特殊化のための逃げ道は、抑制ではなくジェネリクスが第一である: 親を有界の型パラメータ（interface _Consumer[T < Message]）で宣言し、部分型にそれをバインドさせる（include _Consumer[SendMailMessage]）ことで、オーバーライドがインスタンス化された契約に一致するようにする — PHPStanがGenerics in PHP using PHPDocsで手を伸ばすのと同じ解決である（「Barbara Liskovでさえこれに満足している」）。第二は、宣言されたパラメータを広く保ち、狭い型を本体内でoccurrence typingを通じて回復することである。# rigor:disable def.override-*は最後の手段だ。

Rigorが（LSP的に）チェックしないこと

完全性のため、Rigorがv0.1.xで静的に強制しないLSPの義務を — 探すのをやめられるようにここで名指しする:

クロス階層のオーバーライド互換性の推論側。出荷済みのdef.override-*ファミリー（前述の§「クロス階層のオーバーライド互換性」）は両側が著作されたシグネチャを持つことにゲートされている。補完的なケース — 子の推論された戻り値を著作された親の戻り値に対してチェックすること（ADR-35スライス5） — に加えて、RBSのみの祖先へのリーチとシングルトン（def self.）メソッドのカバレッジは保留のままである（需要駆動、より高い偽陽性サーフェス）。
例外互換性。シグネチャ規則の「部分型に新しい例外を入れない」はチェックされない。Rigorは内部の例外/非局所脱出効果（§「エフェクトシステム」）を持つが、メソッドごとのraise集合を表面化させたり、オーバーライド間で比較したりはしない。RBSにはチェック対象となる広く使われたraises句がない。
振る舞い的な事前/事後条件の式（契約による設計）。Meyerスタイルのrequire / ensureの述語契約と、その継承規則には、Rigorのサーフェスがない。最も近いアナログは、型レベルでのリファインメントキャリア（non-empty-string、positive-int、……）とRBS::Extendedの述語ディレクティブだが — どちらも一般的な契約の式ではない。
部分型付けのチェックとしての履歴制約。ファクト安定性 + frozen?を通じて運用的に尊重される（§「不変条件」）。階層レベルの規則としては強制されない。
クラス階層をまたいだ不変条件の推論。宣言サーフェスがなく、ASTを歩く包絡線の外側である。

これらのいずれかがユーザーベースにとって重要になれば、いかなる実装スライスの前にもADRで議論される — 型理論の付録の§「Rigorがモデル化しないこと」が記録するのと同じ規律である。

短い読書リスト

Liskov, B. “Data Abstraction and Hierarchy.” OOPSLA ‘87 Addendum / SIGPLAN Notices, 1988. 置換の直観を述べた基調講演。
Liskov, B. & Wing, J.M. “A Behavioral Notion of Subtyping.” ACM TOPLAS, 1994. 厳密な定式化 — シグネチャ規則 + 事前/事後条件/不変条件/履歴の振る舞い規則。このページのすべての典拠。
Meyer, B. Object-Oriented Software Construction, 2nd ed. Prentice Hall, 1997. 契約による設計と、require / ensure / invariantの継承規則 — 契約規律として述べられた振る舞い規則。
Cardelli, L. & Wegner, P. “On Understanding Types, Data Abstraction, and Polymorphism.” ACM Computing Surveys, 1985. シグネチャ規則が言い表される分散と部分型付けの語彙。
Metz, S. Practical Object-Oriented Design in Ruby（POODR）. Addison-Wesley, 2nd ed. 2018. SOLIDの「L」のRubyコミュニティによる言明 — 型理論不要の、実践的な設計テストとしての置換可能性。
併せて、同伴の§「ロバストネス原則（型のためのPostelの法則）」（規範的）とADR-5（根拠）も参照 — このページがLSPを写し取るRigorのサーフェスである。

次に読むもの

付録 — 型理論との接続 — このページが依拠する形式的足場（分散、漸進的保証、self型 / F有界多相、健全性対完全性のトレードオフ）について。
第6章 — クラス — インスタンス側対クラス側の型付け、self、Data.define — LSPが扱うオブジェクト指向のサーフェス。
第7章 — RBSとRBS::Extended — def.return-type-mismatchがチェックする相手の宣言された契約を著作することについて。
第8章 — エラーを理解する — def.return-type-mismatch / call.argument-type-mismatchのルールと重大度プロファイルについて。

原則ではなく別のツールと比較したい場合は、姉妹の付録がTypeScript、PHPStan、mypy / Pyright、Steepをカバーする。