エンジニアリング哲学：バーバラ・リスコフ、契約こそが型である

要点

• 抽象とは構造ではなく振る舞いに関わるものです。 型とはそれが守る契約――つまり操作とその意味――であって、内部に蓄える bit ではありません。物事はその約束によって使うのであり、その表現によって使うのではないのです。
• サブタイプはスーパータイプの約束を果たさなければなりません。 リスコフの置換原則とは、スーパータイプが期待される場所ではどこでも、サブタイプが呼び出し側の前提を壊さずに機能しなければならないというものです――より弱い事前条件、より強い事後条件、保たれる不変条件。
• モジュール性とは、全体を抱えずに部分を推論できることです。 リスコフの厳密な定義によれば、依存先が契約を守ると信頼したうえで、モジュールを単独で理解し検証できる――その信頼を正当なものにするのが抽象なのです。
• 彼女はデータ抽象をプログラミングの基本要素にしました。 CLU から Argus、そして2008年のチューリング賞まで、一つの考えがデータ構造から分散データベースへと拡大していきます――契約を定義し、仕組みを隠す。

原則

「φ(x) を型 T のオブジェクト x について証明可能な性質とする。このとき、S が T のサブタイプであるならば、型 S のオブジェクト y について φ(y) が真であるべきである。」 – バーバラ・リスコフ、ジャネット・ウィング¹

ゆっくり読んでみてください。これが、いまや分野全体がリスコフの置換原則と呼ぶものの形式的な記述であり、1994年のジャネット・ウィングとの共著論文から来ています。¹ 記法を取り払えば、ほとんど厳しいとも言える主張が残ります。サブタイプは人を驚かせてはならない、というものです。スーパータイプについて証明できたことは、代わりにサブタイプをプログラムに渡したときも真であり続けなければなりません。サブタイプが継承するのは親の約束であって、その形だけではないのです――そしてその約束を守れないなら、型チェッカーが何と言おうと、それはサブタイプではありません。

その厳しさの背後にあるのは、リスコフが40年にわたって追い続けた一つの考えの到達点です。型はその表現ではなく、振る舞いによって定義される。 モジュールとは契約――意味を定められた操作の集合――であり、契約の存在意義はまさに、どう作られているかを読まずにその物事を使えるという点にあります。置換可能性とは、その信念を継承に当てはめただけのものです。S が T の一種だと主張するなら、T が約束されていた場所すべてで、S は同じ約束を果たさなければなりません。構造は違っていてかまいません。振る舞いは違ってはいけないのです。

これがなぜ重要かという問いは、彼女のキャリア全体を貫く糸です。大規模なプログラムが扱えるものになるのは、全体を頭に抱えずに一つの部分を推論できる場合に限られます。リスコフはそれをモジュール性と呼び、その言葉に厳密な意味を込めていました。すなわち、依存するものすべてが定められた契約を守ると信頼したうえで、モジュールを単独で理解し検証できる能力です。その信頼を正当なものにするのがデータ抽象であり、継承がそれをひそかに壊さないようにするのが振る舞いのサブタイプ化なのです。これは、優れたシステムとは吟味できる技術的な仕組みとしての美意識――コードベース全体を読んで吸収する伝統ではなく、述べて確認できる契約――の上に築かれるという主張の根底に流れているのと、同じ信念です。

背景

バーバラ・ジェーン・ヒューバーマン・リスコフは1939年11月7日、カリフォルニア州ロサンゼルスに生まれました。² 1961年、カリフォルニア大学バークレー校で数学を専攻し、物理学を副専攻として学士号を取得します。² バークレーとプリンストンの数学大学院に出願したとき、プリンストンは女性をまったく受け入れていませんでした。そこで彼女は就職の道を選び、ほとんど偶然のように初期のコンピューティングへと入り込んでいきます。Mitre Corporation や Harvard でプログラミングに携わったのち、やはり博士号を取りたいと心を決めたのです。²

1968年、彼女はスタンフォードで博士号を取得しました――計算機科学の学科から博士号を授与された、アメリカで最初の女性のひとりです。² 指導教官は Lisp の発明者であり、人工知能という分野の創始者のひとりでもあるジョン・マッカーシーでした。博士論文ではチェスの終盤を指すプログラムを作り、その過程でキラーヒューリスティック――ゲーム木探索でいまも使われる手の順序付けの工夫――を考案しています。² この細部は心に留めておく価値があります。彼女はその語を生み出した当人のもとで AI から出発し、そののち自らを決定づける問題へと向き直ったのです――機械にいかに考えさせるかではなく、大規模なプログラムをいかに理解可能にするか、という問題へ。

スタンフォードののち、彼女は Mitre に戻り、Venus オペレーティングシステムの設計を率いました――入念な機械とソフトウェアのアーキテクチャがいかにシステムを単純化しうるかを探るために作られた、小規模で低コストの対話型タイムシェアリングシステムです。²³ 1972年には MIT の教員に加わり、以来ずっとそこに留まって、いまでは同校が授ける最高位である Institute Professor を務めています。² Venus は彼女に問いを教えました。1970年代初頭のソフトウェア危機の不安――プログラムが、もはや誰も推論しきれないほど大きくなったという気づきの芽生え――が、その問いを研ぎ澄ましたのです。その答えが CLU になりました。

仕事

データ抽象と CLU 言語

1973年から、リスコフと MIT の学生たちは CLU を設計し構築しました。これは、これまで作られた言語のなかでもとりわけ静かに影響を及ぼしてきた言語のひとつです――本番コードを書いた人はほとんどいないのに、その考えはいまやほぼあらゆる言語に入り込んでいます。⁴ その中心概念がクラスタであり、言語名もそこから取られています。クラスタとは、データ表現とそれに許される操作とを一つに束ね、その操作の集合の背後に表現を完全に隠す単位です。⁴ クラスタは抽象データ型を具体的に実現したものでした――型は、それが何をするかによってのみ利用者に知られるべきで、bit をどう蓄えるかによって知られてはならない、という考えです。⁴⁵

CLU はそこで止まりませんでした。いまでは当たり前となった一群の機能を、先駆けて導入し、あるいは広めたのです。イテレータは yield 文を持つコルーチンとして実装され、コレクションの内部構造を露わにせずにそれを辿れるようにしました。signal と except による構造化された例外処理は、後付けではなく通常の制御フローの一部として扱われました。パラメトリック多相――制約付きの型安全なパラメータ化された型であり、ジェネリクスの先祖です。型安全なバリアント型。そして並列代入による複数の戻り値。⁴ イテレータは Python、C#、Ruby に再登場しました。パラメータ化された型は Java と C# のジェネリクスになりました。例外処理は Java と C++ を形づくりました。Swift の設計者たちは CLU を名指しで挙げています。⁴ この言語は種子の貯蔵庫でした。

しかし機能は原則の下流にあるものでした。リスコフの主張は、抽象とは複雑さを御するための仕組みであるというものでした――難しいものは、きれいな境界を定め、そこを横切るものを規定し、そのうえで両側を同時に考えずに済むようにすることで作るのです。CLU は、プログラミング言語がその境界を単に許すのではなく、強制できるという証明でした。コンパイラが契約の味方になったのです。

リスコフの置換原則

1987年、リスコフは OOPSLA で「データ抽象と階層」と題した基調講演を行い、翌年それは SIGPLAN Notices に掲載されました。⁶ オブジェクト指向プログラミングが台頭しつつあり、それとともにサブタイプ――他の型を継承し拡張する型――という考えも広まっていました。リスコフの問いは、誰も正確には述べていなかった当然のものでした。サブタイプをそのスーパータイプとして扱って、実際に安全なのはいつなのか。講演自身の言葉による彼女の答えは、置換に関する性質でした。「ここで求められているのは、次のような置換の性質である。型 S の各オブジェクト o1 に対して、T を用いて定義されたすべてのプログラム P において o2 を o1 で置き換えても P の振る舞いが変わらないような型 T のオブジェクト o2 が存在するならば、S は T のサブタイプである。」⁶

至るところで目にする通俗的な言い換え――「S が T のサブタイプであるなら、型 T のオブジェクトは、プログラムの望ましい性質を一切損なうことなく型 S のオブジェクトで置き換えられる」――は、それを忠実に圧縮したものです。⁷ 1994年、リスコフとジャネット・ウィングは論文「サブタイプの振る舞い的概念」でそれを厳密にし、真のサブタイプが満たすべき条件を与えました。そのメソッドはスーパータイプのメソッドより多くを要求してはならず（より弱いか等しい事前条件）、より少なくしか約束してはならない（より強いか等しい事後条件）、そしてスーパータイプの不変条件と履歴性質を保たなければなりません。¹ これらの条件をまとめたものが、振る舞いのサブタイプ化の意味するところです――そしてこれこそ、俗な「アヒルのように見えてアヒルのように鳴くなら」式の言い回しが彼女のものでなく、要点を外している理由です。見た目や鳴き声は形であり、原則が問うのは守られた約束だからです。

古典的な反例は、長方形を継承する正方形です。Rectangle では幅と高さを別々に設定でき、クライアントは高さを設定しても幅は変わらないと信じてよいはずです。それを継承する Square は二つを等しく保たせなければなりません――だから高さを設定するとひそかに幅も変わり、クライアントの妥当な前提が破られるのです。⁷ その正方形は辞書的な意味では長方形であるし、あらゆる型チェックを通りますが、それでも振る舞いのサブタイプではありません。長方形の約束を守れないからです。教訓のすべてが、この一つの形に収まっています。構造の継承は、契約の継承ではないのです。

分散システム：Argus と Thor

リスコフは言語設計に留まりませんでした。1980年代初頭、彼女は Argus を構築します。これは、分散プログラム――独立して故障する複数の機械にまたがって走るプログラム――の実装を支援する最初の高水準言語と評されるものです。²³ CLU の拡張である Argus は、ガーディアン（分散状態をカプセル化し、ハンドラを通じてアクセスされるオブジェクト）とアトミックアクション（故障をまたいでも全体が完了するか、まったく行われないかのいずれかとなり、二相コミットで調停されるトランザクション）を導入し、さらにプロミスパイプライニング――呼び出しを発行し、その結果が返る前に作業を続けられる仕組み――を実証しました。⁹ 分散の難問は部分故障です――他のノードが生きているなかで一つのノードが死ぬ――そして Argus はそこにデータ抽象を持ち込みました。ガーディアンとは、ネットワークが守らないときでも保たれる契約なのです。

1990年代の Thor は分散オブジェクト指向データベースで、多くの言語で書かれたプログラムからアクセスされるオブジェクトを、信頼性が高く可用性の高い形で永続的に格納するものでした。²³ CLU からの一貫した流れは寸分の狂いもありません。クラスタは操作の背後に表現を隠し、ガーディアンはアトミックな操作の背後に分散状態を隠し、Thor のオブジェクトは型付きのインターフェースの背後に永続性を隠します。あらゆる規模で――データ構造、ネットワークサービス、データベース――リスコフの一手は同じです。契約を定義し、仕組みを隠し、システムの残りには契約だけを推論させるのです。

2008年チューリング賞と遺産

2009年、ACM はリスコフに2008年の A.M. チューリング賞――コンピューティングの最高栄誉――を授与し、その表彰文にはこうありました。「プログラミング言語とシステム設計の実践的および理論的基盤への貢献、とりわけデータ抽象、フォールトトレランス、分散コンピューティングに関する貢献に対して。」⁸ 拡張された表彰文は、その一貫した流れを正確に名指しています。彼女は「データ抽象、モジュール性、フォールトトレランス、永続性、そして分散コンピューティングシステム」を前進させました。⁸ それ以前にも、彼女は2004年に「プログラミング言語、プログラミング方法論、分散システムへの根本的な貢献に対して」IEEE ジョン・フォン・ノイマン・メダルを受け、のちに全米発明家殿堂入り（2012年）を果たし、ベンジャミン・フランクリン・メダル（2023年）を授与されています。²

その遺産は、指し示して走らせられる言語やシステムではありません。現役のプログラマがいま考える流儀――「インターフェースに対してプログラムせよ」「実装ではなく契約に依存せよ」「このクラスは LSP に違反している」――が、リスコフの語彙であり、あまりにも完全に吸収されたために、それを使う人のほとんどが論文を読んだことすらないという、その事実こそが遺産なのです。これは最も深い種類の影響です。あなたの考えが空気になってしまったがゆえに、もはや誰の名にも帰されなくなるときの影響です。

方法

その方法は30年にわたって一貫しています――オペレーティングシステム、言語設計、分散データベースを通じて。

型をその表現ではなく、振る舞いによって定義する。 繰り返される一手は、境界を引き、そこを横切るものを正確に規定し、そのうえでどちら側も相手の内部に依存させないことです。クラスタ、ガーディアン、Thor のオブジェクトはすべて同じ行為です――仕組みを隠す契約なのです。⁴⁵

モジュール性を文字どおりにし、そのうえで強制する。 リスコフにとってモジュール性とは、コードの整理の好みではありません――依存先が契約を守ると信頼したうえで、モジュールを単独で推論できる能力です。CLU のコンパイラは抽象の壁を礼儀正しく示唆するのではなく、強制しました。規律は、道具が確認してくれて初めて本物になるのです。⁴

サブタイプはスーパータイプの約束を守らなければならない。 振る舞いのサブタイプ化とは、継承が利便ではなく契約であるという原則です。より弱い事前条件、より強い事後条件、保たれる不変条件――サブタイプはより多くを行ってよいが、スーパータイプより多くを要求したり、少なくしか約束しなかったりしては決してならないのです。¹

難問を境界で攻める。 分散システムにおける部分故障が過酷なのは、まさにそれが局所的に推論する能力を壊すからです。Argus の答えは、抽象を故障モデルそのものへと押し込むこと――アトミックアクションとガーディアン――でした。これにより、プログラマはネットワークが崩れうるあらゆる筋道を頭の中で再現せずとも、一つの部分を推論し続けられたのです。²³

一つの考えを最後まで持ち上げる。 スタック、ネットワークサービス、データベースという規模におけるデータ抽象は、まぎれもなく同じ考えです。リスコフは領域ごとに新しい哲学を発明したのではありません。規模に耐える一つを見いだし、それに乗って1970年代の型システムから1990年代の分散ストアまで進んだのです。

影響の連鎖

彼女を形づくった人々

ジョン・マッカーシー。 スタンフォードでの博士課程の指導教官であり、Lisp の発明者にして AI の創始者のひとりである彼は、彼女に数理的な計算機科学の厳密さを与え――そして AI からプログラム構造へと向き直る道を通して――生涯の仕事となる問題を与えました。²（直接の影響）

ソフトウェア危機と構造化プログラミングの時代。 リスコフが研究者として成長したのは、まさにこの分野が、プログラムは人間の理解を超えて大きくなったと認めた時期でした。構造化プログラミング運動――ダイクストラ、ホーア、ヴィルト――は、推論できるようにするには制御フローを規律づけなければならないと主張していました。リスコフは同じ信念をデータへと広げます。プログラムがどう動くかを規律づけるだけでは足りない。そのデータが何を意味し、どう格納されているかを誰が見てよいのかを、規律づけなければならないのです。（形成的な影響）

C.A.R. ホーアと仕様の規律。 事前条件、事後条件、不変条件に関するホーアの仕事――プログラムを論理的な表明として推論すること――は、彼女とウィングが厳密にした振る舞いのサブタイプ化の条件の、直接の知的祖先です。（形成的な影響）

彼女が形づくった人々

あらゆる現代の型システム。 Java と C# のジェネリクス、Python と C# のイテレータ、C 系全体にわたる例外処理、Swift の設計――CLU が先駆けた機能は、いまやほぼあらゆる言語の標準的な調度品です。⁴

オブジェクト指向の実践。 「実装ではなくインターフェースに対してプログラムせよ」、依存関係逆転、そして SOLID という語彙全体の「L」は、リスコフの原則を実務に落とし込んだものです。一世代が、それが誰の考えかを学ぶことなく、悪い派生クラスを見抜けるようになりました。⁷

分散システムのエンジニアリング。 アトミックアクション、故障するノードをまたいだトランザクション的保証、そしてリモートサービスを部分故障を生き延びる契約として扱う実践は、Argus と Thor をさかのぼります。²³

一貫した流れ

エドガー・ダイクストラは、人間が推論できるようにプログラムは構造化されねばならないと主張しました――構造化プログラミングとは、正しさのために制御フローを規律づけることでした。リスコフはその直接の系譜にあります。彼女はダイクストラが制御に対して行ったことをデータに対して行い、モジュール的な推論には規律ある抽象の壁が必要であって、規律あるループだけでは足りないと説いたのです。そしてトンプソンとリッチーが「一つのことをうまくやる」小さな部品を中心に Unix と C を築き、それらをきれいなインターフェースで組み合わせたのに対し、リスコフはその組み合わせがなぜ信頼できるのかという理論を与えました。頼れる部品とは、その契約を述べることができ、そのサブタイプがそれを守るような部品なのです。グレース・ホッパーのコンパイラさえ抽象の行為でした――翻訳を機械の中に移し、人間が自分の言葉で推論できるようにしたのです。リスコフは、抽象そのものを、コンパイラが提供する利便ではなく、プログラム設計の単位にしたのでした。（シリーズの橋渡し）

ここから受け取るもの

私が手放さずにいる教訓は、インターフェースとは約束であり、何かの値打ちがあるインターフェースとは、実際に守るものだけだ、ということです。型シグネチャを書くのは簡単です。難しいのは、そのシグネチャが含意するすべてを果たし、新しい派生クラスやリファクタリングのもとで決してひそかに破らないことです。リスコフの原則は、私が境界に課す基準です――「型チェックは通るか」ではなく、「呼び出し側は、どう作られているかを読まずに、親が信頼されていたあらゆる場所でこの物事を信頼できるか」を問うのです。これは品質こそが唯一の変数であるというのと同じ基準です――問いは決して、コードがコンパイルされるかどうかではなく、契約が本物かどうかなのです。

私がいま作っている世界――エージェント、ツールのループ、AI システム――では、リスコフの信念はかつてないほど重みを担っています。私が組み合わせる部品は、その性質からして不透明だからです。ツール、サブエージェント、モデル呼び出しはモジュールです。契約に基づいてそれを呼び出すのであって、その内部を読むことはできません。勝負のすべては、その契約が保たれるかどうか――「コードベースを検索する」と謳うツールが、その仕様が約束したものを実際に返すのか、それとも一つのモデルを別のものに差し替えると、システムの残りが頼っていた事後条件がひそかに弱まるのか――にかかっています。それこそが、2026年の衣をまとったリスコフの置換原則です。差し替えられた部品は、それが取って代わったものの約束を守らなければなりません。契約を述べ、サブタイプがそれを守るかを確認するという規律は、証拠の関門を単なるスローガン以上のものにする規律とまったく同じです――それぞれの部品が約束を守るからこそ、断片ごとに推論できるシステムなのです。

FAQ

バーバラ・リスコフのエンジニアリング哲学とは何ですか？

リスコフの核心にある信念は、型はその表現ではなく振る舞いによって定義され、それこそが大規模なプログラムを扱えるものにするというものです。モジュールとは契約――意味が定められた操作の集合――であり、契約の目的は、どう作られているかを理解せずにモジュールを使えるという点にあります。このデータ抽象の考えは、CLU 言語から Argus 分散システムに至るまで、彼女が築いたすべてを貫いており、最も有名な成果を生みました――サブタイプはスーパータイプが交わすあらゆる約束を果たさなければならないという原則です。⁴⁵¹

リスコフの置換原則とは何ですか？

それは、サブタイプが、呼び出し側の前提を壊すことなく、スーパータイプが期待されるあらゆる場所で使えなければならないという要請です。形式的には、リスコフとウィングの1994年の記述によれば、「φ(x) を型 T のオブジェクト x について証明可能な性質とする。このとき、S が T のサブタイプであるならば、型 S のオブジェクト y について φ(y) が真であるべきである。」¹ 1987年の OOPSLA 基調講演で、彼女はこれを置換の性質として述べました。型 S のオブジェクトを型 T のオブジェクトに代入しても、あらゆるプログラムの振る舞いが変わらないなら、S は T のサブタイプである、と。⁶ 実務上、真のサブタイプはスーパータイプより多くを要求してはならず（より弱いか等しい事前条件）、より少なくしか約束してはならず（より強いか等しい事後条件）、その不変条件を保たなければなりません。俗な「アヒルのように見えるなら」式の言い回しはリスコフのものではなく、要点を外しています。原則が問うのは守られた約束であって、表面的な類似ではないのです。⁷

バーバラ・リスコフは何を発明しましたか？

彼女は CLU プログラミング言語（1973年開始）の設計を行い、その実装を率いました。CLU は抽象データ型、イテレータ、構造化された例外処理、パラメトリック多相を導入あるいは広めた言語で――これらの機能はいまや Java、C#、Python、Swift をはじめとする言語の標準です。⁴ それ以前には Venus タイムシェアリングオペレーティングシステムを構築し、のちには分散プログラムのための最初の高水準言語である Argus と、分散オブジェクト指向データベースの Thor を生み出しました。²³ ジャネット・ウィングとともに、いまリスコフの置換原則と呼ばれる振る舞いのサブタイプ化を形式化しています。¹

バーバラ・リスコフはなぜチューリング賞を受賞したのですか？

ACM は彼女に2008年の A.M. チューリング賞を「プログラミング言語とシステム設計の実践的および理論的基盤への貢献、とりわけデータ抽象、フォールトトレランス、分散コンピューティングに関する貢献に対して」授与しました。⁸ その評価は彼女のキャリア全体に及びます――CLU を通じてデータ抽象をプログラミング言語の基本要素にしたこと、モジュール性とサブタイプ化の理論を前進させたこと、そしてそれらの考えを、独立して故障する機械をまたいで信頼できるシステムを築くという難問に持ち込んだこと。彼女はアメリカで最初に計算機科学の博士号を取得した女性のひとりであり（スタンフォード、1968年）、MIT の Institute Professor を務めています。²

出典