工程哲學：Barbara Liskov，契約即型別

關鍵要點

• 抽象關乎行為，而非結構。 型別就是它所信守的契約——是那些操作及其意義，而非它儲存的位元。您透過事物的承諾來使用它，絕不透過它的表示方式。
• 子型別必須兌現父型別的承諾。 這就是Liskov替換原則（Liskov Substitution Principle）：凡是預期出現父型別的地方，子型別都必須能正常運作而不破壞呼叫者的假設——更寬鬆的前置條件、更嚴格的後置條件、保持不變的不變式。
• 模組化意味著無需顧及全局即可推理局部。 Liskov給出的精確定義是：您能孤立地理解並驗證一個模組，並信任它的依賴項各自信守契約。抽象正是讓這份信任站得住腳的根據。
• 她讓資料抽象成為程式設計的基本要素。 從CLU到Argus，再到2008年的圖靈獎，同一個構想能從一個資料結構一路擴展到一個分散式資料庫：定義契約，隱藏機制。

原則

「令φ(x)為一項關於型別T之物件x可證明的性質。那麼對於型別S之物件y（其中S為T的子型別），φ(y)亦應為真。」——Barbara Liskov與Jeannette Wing¹

慢慢讀，這就是如今整個領域所稱的Liskov替換原則的形式化陳述，出自她1994年與Jeannette Wing合著的論文。¹ 剝去那些符號，它說的是某種近乎嚴厲的東西：子型別不被允許讓您意外。凡是您能就父型別證明為真的事，當程式拿到的是子型別時也必須維持為真。子型別繼承的是父型別的承諾，而不只是它的外形——倘若它無法信守這些承諾，那它就不是子型別，無論型別檢查器怎麼說。

這份嚴厲的背後，是Liskov追尋了四十年的單一構想的集大成：型別由其行為定義，而非由其表示定義。 一個模組就是一份契約——一組具有指定意義的操作——而契約的全部要點在於，您能使用這個事物而無需去讀它是如何打造的。可替換性不過是把這份信念套用到繼承之上：如果S聲稱自己是T的一種，那麼凡是承諾過T的地方，S就必須信守同一份承諾。結構可以不同，行為不能。

這之所以重要，是貫穿她整個職業生涯的那條線索：唯有當您能在不把全局都裝進腦袋的情況下推理某一部分時，大型程式才是可駕馭的。Liskov用來指稱這件事的詞是模組化，而她對它有著精確的含義：孤立地理解並驗證一個模組的能力，並信任它所依賴的一切都會信守其所聲明的契約。資料抽象正是讓這份信任站得住腳的根據，而行為子型別化則是讓繼承不至於悄悄破壞它的東西。這正是同一份信念，撐在那個論點底下——好的系統之所以被打造出來，是為了讓品味成為一套您能檢視的技術系統——一份您能陳述並核對的契約——而非一套您得讀完整個程式碼庫才能吸收的傳統。

背景

Barbara Jane Huberman Liskov於1939年11月7日生於加州洛杉磯。² 她於1961年取得加州大學柏克萊分校的數學學士學位，副修物理。² 當她申請柏克萊與普林斯頓的數學研究所時，普林斯頓根本不收女性；於是她改去工作，幾乎是誤打誤撞地踏入早期的計算領域，先後在Mitre公司與哈佛從事程式設計，最終才決定她終究還是想要那個博士學位。²

她於1968年取得史丹佛的博士學位——是美國最早從電腦科學系獲得博士學位的女性之一。² 她的指導教授是John McCarthy，Lisp的發明者，也是人工智慧這個領域的奠基者之一；她的博士論文打造了一個下西洋棋殘局的程式，而在這過程中她設計出了殺手啟發法（killer heuristic），一種至今仍用於賽局樹搜尋的著法排序技巧。² 這個細節值得記住：她是從AI出身的，師承那位創造這個術語的人，而後卻轉身離開它，奔向那個將會定義她一生的問題——不是如何讓機器思考，而是如何讓一個大型程式可理解。

離開史丹佛後她回到Mitre，在那裡主導了Venus作業系統的設計——一個小型、低成本的互動式分時系統，打造它是為了探究審慎的機器與軟體架構能如何簡化一個系統。²³ 1972年她加入MIT教職，自此一直留在那裡，如今是該校所授予的最高職銜——Institute Professor。² Venus教會了她那個問題。1970年代初的軟體危機焦慮——人們漸漸意識到程式已大到無人能對其推理——讓這個問題更加尖銳。而答案，成了CLU。

工作

資料抽象與CLU語言

自1973年起，Liskov與她在MIT的學生們設計並打造了CLU，而它是有史以來最低調卻最具影響力的語言之一——一個幾乎沒人拿來寫產品程式碼的語言，它的構想如今卻幾乎無處不在。⁴ 它的核心組織概念是cluster（叢集），語言之名即由此而來：一個把資料表示與其所允許的操作捆綁在一起的單元，並將表示完全隱藏在那組操作之後。⁴ cluster是抽象資料型別（abstract data type）的具體實現——也就是這樣一個構想：一個型別對其使用者而言，只應以它做什麼為人所知，絕不以它如何儲存位元為人所知。⁴⁵

CLU並未止步於此。它開創或推廣了一整批如今已是基本配備的卓越特性：迭代器（iterator），以協程加上一個yield敘述句來實作，讓您能走訪一個集合而不暴露它的內部結構；以signal與except構成的結構化例外處理，被視為正常控制流程的一部分，而非事後加裝上去的；參數化多型（parametric polymorphism）——帶有約束的型別安全參數化型別，是泛型的祖先；型別安全的變體型別；以及透過平行賦值達成的多重回傳值。⁴ 迭代器後來重現於Python、C#與Ruby。參數化型別成了Java與C#裡的泛型。例外處理形塑了Java與C++。Swift的設計者更指名感謝CLU。⁴ 這個語言是一座種子庫。

但這些特性都是原則的下游產物。Liskov的論點是，抽象正是我們用以駕馭複雜性的機制——您打造一件困難的事物，靠的是劃出一道清晰的邊界、明定什麼跨越它，然後就再也不必同時去想邊界的兩側。CLU證明了一門程式語言能夠強制那道邊界，而不只是容許它。編譯器成了契約的盟友。

Liskov替換原則

1987年，Liskov在OOPSLA發表了一場題為「Data Abstraction and Hierarchy」的主題演講，隔年刊載於SIGPLAN Notices。⁶ 當時物件導向程式設計正如日中天，隨之而來的是子型別的構想——繼承自其他型別並加以擴充的型別。Liskov提出的，是那個顯而易見卻無人精確陳述過的問題：究竟在什麼時候，把一個子型別當作它的父型別來對待才真正安全？她的答案，用這場演講自己的話來說，是一項替換性質：「這裡想要的是某種如下的替換性質：若對型別S的每個物件o1，都存在一個型別T的物件o2，使得對所有以T為定義基礎的程式P而言，當o1替換o2時P的行為維持不變，那麼S便是T的子型別。」⁶

您到處都會看到的那個通俗轉述——「若S是T的子型別，那麼型別T的物件可以被型別S的物件取代，而不改變程式任何令人期望的性質」——是對它忠實的壓縮。⁷ 1994年，Liskov與Jeannette Wing在論文「A Behavioral Notion of Subtyping」中讓它變得嚴謹，給出了一個真正的子型別必須滿足的條件：它的方法要求的不能更多（更寬鬆或相等的前置條件），承諾的不能更少（更嚴格或相等的後置條件），且它必須保持父型別的不變式與歷史性質。¹ 這些條件合在一起，正是行為子型別化的含義——而它們也正是為什麼那些口語化的「如果牠看起來像鴨子、叫起來像鴨子」式的說法並非出自她、且未抓住要點的原因：看起來與叫起來都是外形；這個原則講的是信守承諾。

那個經典的反例，是繼承自矩形的正方形。一個Rectangle讓您各自獨立地設定寬與高；客戶端可以設定高度，並信任寬度不變。一個繼承自它的Square卻必須強迫兩者相等——於是設定高度會悄悄改變寬度，呼叫者那個合情合理的假設因而被破壞。⁷ 這個正方形在字典意義上是一個（is-a）矩形，也通過每一項型別檢查，卻仍然不是行為子型別，因為它無法信守矩形的承諾。整個教訓就坐落在那一個形狀裡：繼承了結構，不等於繼承了契約。

分散式系統：Argus與Thor

Liskov並未停留在語言設計。1980年代初，她打造了Argus，被描述為第一個支援分散式程式實作的高階語言——所謂分散式程式，是散佈在各自獨立故障的機器上的程式。²³ Argus是CLU的延伸，引入了guardian（守護者，封裝分散式狀態、透過handler存取的物件）與atomic action（原子動作，即要麼完整完成、要麼全不發生的交易，即使跨越故障也是如此，由兩階段提交協調），並展示了promise pipelining（承諾管線化），讓您能發出一個呼叫，並在它的結果回傳之前就繼續工作。⁹ 分散式的難題在於部分故障——一個節點死去，而其餘節點仍存活——而Argus把資料抽象拿來應對它：一個guardian就是一份契約，即使網路撐不住時它依然成立。

1990年代的Thor，是一個分散式物件導向資料庫，為以多種語言編寫的程式所存取的物件，提供可靠、高可用的持久性儲存。²³ 那條從CLU貫穿而來的脈絡分毫不差。cluster把表示隱藏在操作之後；guardian把分散式狀態隱藏在原子操作之後；一個Thor物件則把持久性隱藏在一個帶型別的介面之後。在每一種尺度上——一個資料結構、一個網路服務、一個資料庫——Liskov的招式都一樣：定義契約，隱藏機制，讓系統其餘的部分只需就契約來推理。

2008年圖靈獎與傳承

2009年，ACM將2008年的A.M.圖靈獎——計算領域的最高榮譽——頒給Liskov，頒獎詞為：「表彰其對程式語言與系統設計之實務與理論基礎的貢獻，尤其與資料抽象、容錯及分散式計算相關者。」⁸ 那則加長版的頒獎詞精確點出了這條貫穿脈絡：她推進了「資料抽象、模組化、容錯、持久性，以及分散式計算系統」。⁸ 在此之前，她已於2004年獲頒IEEE John von Neumann獎章，「以表彰其對程式語言、程式設計方法論及分散式系統的根本性貢獻」，而後又被選入美國國家發明家名人堂（2012年），並獲頒Benjamin Franklin獎章（2023年）。²

這份傳承並不是一門您能指著它跑起來的語言或系統。它是這樣一件事：如今在職程式設計師思考的方式——「對介面編程」、「依賴契約而非實作」、「這個類別違反了LSP」——就是Liskov的詞彙，被吸收得如此徹底，以至於大多數使用它的人從未讀過那篇論文。這是最深的一種影響力：當您的構想不再被歸於誰名下，因為它已經化作了空氣。

方法

這套方法在三十年間始終如一——橫跨作業系統、語言設計與分散式資料庫。

以行為定義型別，而非以表示定義。 那個反覆出現的招式，是劃出一道邊界，精確明定什麼跨越它，然後拒絕讓任一側去依賴另一側的內部。一個cluster、一個guardian、一個Thor物件，全是同一個動作：一份隱藏了機制的契約。⁴⁵

讓模組化名副其實，然後強制它。 對Liskov而言，模組化不是一種程式碼組織上的偏好——它是孤立地推理一個模組、並信任其依賴項各自信守契約的能力。CLU的編譯器強制了那道抽象屏障，而非客氣地建議它。唯有當工具會去核對時，這套紀律才是真的。⁴

子型別必須信守父型別的承諾。 行為子型別化所秉持的原則是：繼承是一份契約，而非一種便利。更寬鬆的前置條件、更嚴格的後置條件、保持不變的不變式——子型別可以做得更多，但它絕不能要求更多，也不能承諾更少於它的父型別。¹

在邊界上正面迎擊難題。 分散式系統中的部分故障之所以如此殘酷，恰恰是因為它破壞了您在局部推理的能力。Argus的答案，是把抽象推進到故障模型本身之中——原子動作與guardian——好讓程式設計師仍能就某一部分推理，而無需模擬網路可能崩解的每一種方式。²³

把一個構想一路帶到頂。 在一個堆疊、一個網路服務與一個資料庫的尺度上，資料抽象都能被辨認為同一個構想。Liskov並沒有為每個領域發明一套新哲學；她找到了那個能擴展的，然後駕著它，從1970年代的一套型別系統一路騎到1990年代的一個分散式儲存。

影響鏈

形塑她的人

John McCarthy。 她在史丹佛的博士指導教授，Lisp的發明者，也是AI的奠基者，他既給了她數學式電腦科學的嚴謹，也——透過她從AI轉身奔向程式結構的那一回——給了她那個成為她畢生事業的問題。²（直接影響）

軟體危機與結構化程式設計的時代。 Liskov作為研究者成熟的時刻，恰恰是這個領域承認程式已超出人類理解能力之時。結構化程式設計運動——Dijkstra、Hoare、Wirth——主張控制流程必須加以紀律化方能被推理。Liskov把同一份信念延伸到資料上：光是紀律化程式如何移動還不夠；您必須紀律化它的資料意味著什麼，以及誰被允許看見它如何被儲存。（奠基性影響）

C.A.R. Hoare與規格的紀律。 Hoare關於前置條件、後置條件與不變式的工作——把程式當作邏輯斷言來推理——正是她與Wing所精確化的那些行為子型別化條件的直系智識祖先。（奠基性影響）

被她形塑的人

每一套現代型別系統。 Java與C#裡的泛型、Python與C#裡的迭代器、整個C語族的例外處理、Swift的設計——這些由CLU開創的特性，如今已是幾乎每一門語言的預設家具。⁴

物件導向實務。 「對介面編程，而非對實作編程」、依賴反轉，以及整套SOLID詞彙裡那個「L」，全都是Liskov的原則被付諸運作的成果。一整代人學會了一眼認出一個糟糕的子類別，卻從未學過那是誰的構想。⁷

分散式系統工程。 原子動作、跨越故障節點的交易保證，以及把一個遠端服務當作一份能挺過部分故障的契約來對待的做法，都能循著Argus與Thor回溯而上。²³

貫穿脈絡

Edsger Dijkstra主張，一個程式必須被結構化，好讓人類能對它推理——結構化程式設計就是服務於正確性的控制流程紀律。Liskov是那條直系血脈：她為資料做了Dijkstra為控制所做的事，堅持模組化推理需要的是有紀律的抽象屏障，而不只是有紀律的迴圈。而當Thompson與Ritchie圍繞著「把一件事做好」並透過乾淨介面組合的小型元件打造了Unix與C，Liskov則給出了為什麼那種組合值得信賴的理論：一個您能仰賴的元件，是那種其契約您能陳述、且其子型別會信守它的元件。就連Grace Hopper的編譯器也是一樁抽象之舉——把翻譯搬進機器裡，好讓人類能以自己的語彙推理；而Liskov讓抽象本身成了程式設計的單元，而非編譯器所提供的一種便利。（系列銜接）

我從中汲取的

我一直記著的教訓是：介面是一個承諾，而唯一有價值的介面，是您真正信守的那些。寫出一個型別簽章很容易；難的是兌現那個簽章所蘊含的一切，並在一個新的子類別或一次重構之下，從不悄悄違背它。Liskov的原則，是我用來衡量一道邊界的標準：問的不是「型別檢查過不過？」而是「呼叫者能否在凡是其父型別曾被信任的每個地方，都信任這個東西，而無需去讀它是如何打造的？」這跟品質是唯一的變數是同一道門檻——問題從來不是程式碼能否編譯，而是那份契約是否為真。

在我如今所打造的世界裡——代理人（agent）、工具迴圈、AI系統——Liskov的信念比以往任何時候都更具承重作用，因為我所組合的元件本質上就是不透明的。一個工具、一個子代理人、一次模型呼叫，都是一個模組：您依著一份契約去調用它，而您無法去讀它的內部。整場賽局，就在於那份契約是否成立——一個聲稱會「搜尋程式碼庫」的工具，是否真的回傳了它的規格所承諾的東西，又或者把一個模型換成另一個，是否悄悄削弱了系統其餘部分所依賴的某個後置條件。那正是穿著2026年衣裳的Liskov替換原則：一個被替換進來的元件，必須信守它所取代的那個元件的承諾。陳述契約、並核對子型別是否信守它的這套紀律，正是讓證據門檻不只是一句口號的那套紀律——一個您能分塊推理的系統，因為每一塊都信守它的承諾。

常見問題

Barbara Liskov的工程哲學是什麼？

Liskov的核心信念是：型別由其行為定義，而非由其表示定義，而這正是讓大型程式變得可駕馭的東西。一個模組就是一份契約——一組具有指定意義的操作——而契約的目的在於，您能使用這個模組而無需理解它是如何打造的。這個資料抽象的構想貫穿了她所打造的一切，從CLU語言到Argus分散式系統，並催生了她最著名的成果：子型別必須兌現其父型別所許下的每一個承諾的原則。⁴⁵¹

什麼是Liskov替換原則？

它要求子型別必須能在凡是預期其父型別的任何地方被使用，而不破壞呼叫者的假設。在Liskov與Wing 1994年的陳述中，形式化的說法是：「令φ(x)為一項關於型別T之物件x可證明的性質。那麼對於型別S之物件y（其中S為T的子型別），φ(y)亦應為真。」¹ 在她1987年的OOPSLA主題演講中，她把它表述為一項替換性質：若以型別S的物件替換型別T的物件，會讓每個程式的行為維持不變，那麼S便是T的子型別。⁶ 在實務上，一個真正的子型別要求的不能多於其父型別（更寬鬆或相等的前置條件），承諾的不能更少（更嚴格或相等的後置條件），且必須保持它的不變式。那些通俗的「如果牠看起來像鴨子」式說法並非出自Liskov，且未抓住要點：這個原則講的是信守承諾，而非表面相似。⁷

Barbara Liskov發明了什麼？

她設計並主導實作了CLU程式語言（始於1973年），它引入或推廣了抽象資料型別、迭代器、結構化例外處理與參數化多型——這些特性如今已是Java、C#、Python、Swift等語言的標準配備。⁴ 更早之前她打造了Venus分時作業系統；後來她創造了Argus，第一個用於分散式程式的高階語言，以及Thor，一個分散式物件導向資料庫。²³ 她與Jeannette Wing一同形式化了行為子型別化，如今稱為Liskov替換原則。¹

Barbara Liskov為什麼贏得圖靈獎？

ACM將2008年的A.M.圖靈獎頒給她，「表彰其對程式語言與系統設計之實務與理論基礎的貢獻，尤其與資料抽象、容錯及分散式計算相關者」。⁸ 這份肯定橫跨她的整個職業生涯：透過CLU讓資料抽象成為一項程式語言的基本要素、推進模組化與子型別化的理論，並把那些構想拿來應對一個難題——在各自獨立故障的機器之間打造可靠的系統。她是美國最早取得電腦科學博士學位的女性之一（史丹佛，1968年），如今是MIT的Institute Professor。²

來源