工程哲学:Barbara Liskov,契约即类型

核心要点
- 抽象关乎行为,而非结构。 类型即它所恪守的契约——那些操作及其含义——而不是它所存储的比特。你通过它的承诺来使用它,绝不通过它的表示来使用它。
- 子类型必须兑现父类型的承诺。 这就是 Liskov 替换原则:凡是期望父类型出现的地方,子类型都必须能正常工作,不破坏调用方的假设——更弱的前置条件、更强的后置条件、保持不变的不变量。
- 模块化意味着无需通览整体即可推理某个局部。 Liskov 给出了精确定义:你可以孤立地理解和验证一个模块,并信任它的依赖项会恪守各自的契约。抽象正是让这种信任合理成立的东西。
- 她让数据抽象成为一种编程基本要素。 从 CLU 到 Argus,再到 2008 年的图灵奖,同一个理念可以从一个数据结构一路扩展到一个分布式数据库:定义契约,隐藏机制。
原则
“设 φ(x) 是关于类型 T 的对象 x 可证明成立的某个性质。那么对于类型 S 的对象 y,φ(y) 也应当成立,其中 S 是 T 的子类型。” – Barbara Liskov 与 Jeannette Wing1
慢慢读,这便是如今业界称为 Liskov 替换原则的形式化表述,出自她 1994 年与 Jeannette Wing 合著的论文。1 剥去符号,它说的是某种近乎严苛的东西:子类型不许给你带来意外。凡是你能对父类型证明为真的事情,在你转而把子类型交给程序时都必须保持为真。子类型继承的是父类型的承诺,而不只是它的形态——如果它无法兑现这些承诺,那它就不是子类型,无论类型检查器怎么说。
这份严苛背后,是 Liskov 追寻了四十年的同一个理念的集大成:类型由它的行为定义,而非它的表示。 一个模块就是一份契约——一组具有特定含义的操作——而契约的全部意义在于,你无需读懂它如何构建就能使用它。可替换性正是把这一信念应用到继承上:如果 S 声称自己是某种 T,那么凡是承诺过 T 的地方,S 都必须恪守同样的承诺。结构可以不同。行为不可以。
为什么这至关重要,是贯穿她整个职业生涯的那条主线:大型程序唯有在你能够推理某一部分而无需把整体装进脑海时,才是可驾驭的。Liskov 称之为模块化,而她对这个词有一层精确的含义:能够孤立地理解和验证一个模块,并信任它所依赖的一切都会恪守各自既定的契约。数据抽象正是让这种信任合理成立的东西,而行为子类型正是防止继承悄然破坏它的东西。这与下面这一论点底层的信念别无二致:好的系统之所以被构建出来,是为了让品味成为一套你可以审视的技术系统——一份你可以陈述并核验的契约——而不是一种你靠通读整个代码库来吸收的传统。
背景
Barbara Jane Huberman Liskov 于 1939 年 11 月 7 日出生在加利福尼亚州洛杉矶。2 1961 年,她在加州大学伯克利分校取得数学学士学位,辅修物理。2 当她申请伯克利和普林斯顿的数学研究生项目时,普林斯顿当时根本不招收女性;于是她转而去工作,几乎是机缘巧合地踏入了早期计算领域,先后在 Mitre 公司和哈佛从事编程,之后才决定终究还是要去读博士。2
1968 年,她在斯坦福取得博士学位——是美国最早从计算机科学系拿到博士学位的女性之一。2 她的导师是 John McCarthy,Lisp 的发明者、人工智能领域的奠基人之一;她的博士论文构建了一个下国际象棋残局的程序,过程中她还设计出了杀手启发式(killer heuristic),一种至今仍用于博弈树搜索的着法排序技巧。2 这个细节值得记住:她是从 AI 起步的,师从那个创造了”人工智能”一词的人,而后她转身离开它,奔向那个将定义她一生的问题——不是如何让机器思考,而是如何让一个大型程序可被理解。

斯坦福毕业后她回到 Mitre,在那里领导了 Venus 操作系统的设计——一个小型、低成本的交互式分时系统,旨在探索精心设计的机器与软件架构如何能简化一个系统。23 1972 年她加入 MIT 任教,自此再未离开,如今是该校授予的最高头衔——研究院教授(Institute Professor)。2 Venus 教会了她那个问题。1970 年代初的软件危机焦虑——人们逐渐意识到程序已经庞大到无人能够推理——把这个问题磨得更加锋利。答案最终成了 CLU。
工作
数据抽象与 CLU 语言
从 1973 年起,Liskov 和她在 MIT 的学生们设计并构建了 CLU,它是有史以来影响最为深远却又最不张扬的语言之一——一门几乎无人用来写生产代码的语言,可它的理念如今几乎无处不在。4 它的核心组织概念是簇(cluster),语言之名即由此而来:一个把数据表示与允许施加于其上的操作捆绑在一起的单元,并把表示完全隐藏在那一组操作之后。4 簇是抽象数据类型的具体实现——这一理念主张,一个类型对其使用者而言应当只以它做什么为人所知,而绝不以它如何存储比特为人所知。45
CLU 并未止步于此。它开创或推广了一批如今已成基本门槛的特性:迭代器,以带 yield 语句的协程实现,使你能遍历一个集合而不暴露其内部结构;带 signal 与 except 的结构化异常处理,被当作正常控制流的一部分而非外加的附件;参数化多态——带约束的类型安全参数化类型,泛型的先祖;类型安全的变体类型;以及通过并行赋值实现的多返回值。4 迭代器在 Python、C# 和 Ruby 中重现。参数化类型在 Java 和 C# 中成了泛型。异常处理塑造了 Java 和 C++。Swift 的设计者们曾点名致谢 CLU。4 这门语言是一座种子库。
但这些特性都是原则的下游产物。Liskov 的论点是,抽象正是我们管理复杂度的机制——你构建一件难事的方式,是划定一条清晰的边界,规定什么可以跨越它,然后再也不必同时思考两侧。CLU 证明了一门编程语言可以强制这条边界,而不仅仅是允许它。编译器成了契约的盟友。
Liskov 替换原则
1987 年,Liskov 在 OOPSLA 上作了题为”Data Abstraction and Hierarchy”的主题演讲,次年发表于 SIGPLAN Notices。6 面向对象编程正如日中天,随之而来的是子类型的理念——继承并扩展其他类型的类型。Liskov 提出的,是那个显而易见却无人精确陈述过的问题:究竟在什么情况下,把一个子类型当作它的父类型来对待才是真正安全的?她的答案,用演讲本身的话来说,是一条替换性质:”这里想要的,是某种类似下面的替换性质:若对类型 S 的每个对象 o1,都存在一个类型 T 的对象 o2,使得对所有以 T 定义的程序 P 而言,当用 o1 替换 o2 时 P 的行为保持不变,那么 S 就是 T 的子类型。”6
你随处可见的那个通俗转述——“若 S 是 T 的子类型,则可以用类型 S 的对象替换类型 T 的对象,而不改变程序的任何理想性质”——是对它忠实的压缩。7 1994 年,Liskov 和 Jeannette Wing 在论文《A Behavioral Notion of Subtyping》中将其严格化,给出了一个真正的子类型必须满足的条件:它的方法所要求的不能更多(更弱或相等的前置条件),所承诺的不能更少(更强或相等的后置条件),并且它必须保持父类型的不变量与历史性质。1 这些条件合在一起,正是行为子类型的含义——也正因如此,那些”如果它看起来像鸭子、叫起来像鸭子”的通俗说法并不是她的,而且没抓住要点:看与叫是形态;这一原则讲的是恪守承诺。
经典的反例是继承自矩形的正方形。Rectangle 让你独立地设置宽和高;客户端可以设置高度,并信任宽度不会变。继承自它的 Square 却必须强制二者相等——于是设置高度会悄然改变宽度,客户端那个合情合理的假设便被违背了。7 正方形在字典意义上是一个矩形,能通过每一项类型检查,可它依然不是行为子类型,因为它无法恪守矩形的承诺。整堂课就落在这一个形状里:结构的继承不等于契约的继承。
分布式系统:Argus 与 Thor
Liskov 没有停留在语言设计上。1980 年代初,她构建了 Argus,它被称为第一门支持分布式程序实现的高级语言——分布式程序,即分散在多台会各自独立故障的机器上的程序。23 Argus 是 CLU 的扩展,引入了守护者(guardian,封装分布式状态、通过处理器(handler)访问的对象)和原子动作(atomic action,要么完全完成、要么完全不发生的事务,即便跨越故障也是如此,由两阶段提交协调),并且它展示了承诺流水线(promise pipelining)——你可以发出一个调用,在其结果返回之前就继续工作。9 分布式的难题在于部分故障——一个节点死了而其他节点还活着——而 Argus 把数据抽象用到了这上面:守护者是一份即使网络失守也依然成立的契约。
Thor,诞生于 1990 年代,是一个分布式的面向对象数据库,为以多种语言编写的程序所访问的对象,提供可靠、高可用的持久化存储。23 从 CLU 一脉相承的那条线索精确无比。簇把一个表示隐藏在操作之后;守护者把分布式状态隐藏在原子操作之后;Thor 对象把持久化隐藏在一个带类型的接口之后。在每一种尺度上——一个数据结构、一项网络服务、一个数据库——Liskov 的手法都是同一个:定义契约,隐藏机制,让系统的其余部分只针对契约去推理。

2008 年图灵奖与遗产
2009 年,ACM 将 2008 年的 A.M. 图灵奖——计算领域的最高荣誉——授予 Liskov,颁奖词是:”表彰其对编程语言与系统设计的实践与理论基础所作的贡献,尤其与数据抽象、容错和分布式计算相关。”8 完整颁奖词精确地点出了那条贯穿始终的主线:她推进了”数据抽象、模块化、容错、持久化以及分布式计算系统”。8 在此之前,她已于 2004 年获得 IEEE John von Neumann 奖章,”表彰其对编程语言、编程方法学和分布式系统的根本性贡献”,后来她又入选美国发明家名人堂(2012 年),并获颁本杰明·富兰克林奖章(2023 年)。2
这份遗产不是一门你可以指着运行的语言或系统。它是:如今实战中的程序员们思考问题的方式——“面向接口编程”、”依赖契约而非实现”、”这个类违反了 LSP”——就是 Liskov 的词汇,被吸收得如此彻底,以至于大多数使用它的人从未读过那篇论文。这是最深刻的一种影响:当你的理念不再被归功于你,因为它已经化作了空气。
方法
这套方法在三十年间始终如一——操作系统、语言设计、分布式数据库,概莫能外。
用行为而非表示来定义类型。 反复出现的手法是划一条边界,精确规定什么可以跨越它,然后拒绝让任何一侧依赖另一侧的内部。簇、守护者、Thor 对象,都是同一个动作:一份隐藏机制的契约。45
让模块化落到实处,再去强制它。 对 Liskov 而言,模块化不是一种代码组织上的偏好——它是孤立地推理一个模块、并信任其依赖项恪守各自契约的能力。CLU 的编译器强制那道抽象屏障,而不是客客气气地建议它。唯有当工具会去核验它时,这套纪律才是真实的。4
子类型必须恪守父类型的承诺。 行为子类型这一原则主张:继承是一份契约,而非一种便利。更弱的前置条件、更强的后置条件、保持不变的不变量——子类型可以做得更多,但绝不可要求更多或承诺更少。1
在边界处攻克难题。 分布式系统中的部分故障之所以残酷,恰恰因为它摧毁了你局部推理的能力。Argus 的答案是把抽象推进到故障模型本身之中——原子动作与守护者——使程序员仍能推理某一部分,而无需在脑中模拟网络可能崩解的每一种方式。23
把一个理念一路贯彻到底。 在一个栈、一项网络服务和一个数据库的尺度上的数据抽象,明明白白是同一个理念。Liskov 没有为每个领域发明一套新哲学;她找到了那个能够扩展的理念,并骑着它从 1970 年代的类型系统一直走到 1990 年代的分布式存储。
影响链
谁塑造了她
John McCarthy。 她在斯坦福的博士导师、Lisp 的发明者、AI 的奠基人之一,既给了她数理计算机科学的严谨,也——通过她从 AI 转向程序结构这一转身——给了她那个成为毕生事业的问题。2(直接影响)
软件危机与结构化编程时代。 Liskov 作为研究者成长起来的时刻,恰恰是这个领域承认程序已超出人类理解能力的时刻。结构化编程运动——Dijkstra、Hoare、Wirth——曾论证控制流必须有纪律才能被推理。Liskov 把同一信念延伸到了数据上:仅仅约束程序如何运转是不够的;你还必须约束它的数据意味着什么、谁被允许看到它如何被存储。(奠基性影响)
C.A.R. Hoare 与规约的纪律。 Hoare 关于前置条件、后置条件和不变量的工作——把程序当作逻辑断言来推理——正是她与 Wing 所精确化的那些行为子类型条件的直接思想先祖。(奠基性影响)
她塑造了谁
每一个现代类型系统。 Java 和 C# 中的泛型、Python 和 C# 中的迭代器、整个 C 家族中的异常处理、Swift 的设计——CLU 开创的那些特性,如今已是几乎每一门语言里的默认家什。4
面向对象实践。 “面向接口而非实现编程”、依赖倒置,以及整个 SOLID 词汇表里那个”L”,都是 Liskov 原则被付诸操作的产物。一代人学会了一眼看出糟糕的子类,却从未学到这是谁的主意。7
分布式系统工程。 原子动作、跨故障节点的事务性保证,以及把一个远程服务当作一份能在部分故障中幸存的契约来对待的做法,都可经由 Argus 与 Thor 追溯到她。23
那条贯穿始终的主线
Edsger Dijkstra 论证道,程序必须被构建得让人类能够推理它——结构化编程就是为正确性服务的控制流纪律。Liskov 是这一脉的直接传人:她为数据所做的,正是 Dijkstra 为控制所做的,坚持认为模块化推理需要的是有纪律的抽象屏障,而不只是有纪律的循环。而当Thompson 与 Ritchie 围绕着那些”把一件事做好”、通过干净接口相互组合的小型组件构建起 Unix 与 C 时,Liskov 给出了那份组合为何值得信赖的理论:一个你可以依赖的组件,是一个你能够陈述其契约、且其子类型恪守该契约的组件。即便是Grace Hopper 的编译器也是一次抽象之举——把翻译挪进机器,好让人类能用自己的语汇来推理;Liskov 则让抽象本身成为程序设计的单位,而非编译器提供的一种便利。(系列衔接)
我从中汲取了什么
我留住的那一课是:接口是一个承诺,而唯一值钱的接口,是你真正恪守的那些。写一个类型签名是容易的;难的是恪守那个签名所暗示的一切,并且在一个新的子类或一次重构之下也绝不悄然违背它。Liskov 的原则就是我衡量一道边界的标尺:不是问”类型检查通过了吗?”,而是问”凡是它的父类被信任的地方,调用方都能信任这个东西吗——而无需读懂它如何构建?”这与质量是唯一的变量是同一道标尺——问题从来不是代码能否编译,而是契约是否真实。
在我如今构建的世界里——智能体、工具循环、AI 系统——Liskov 的信念比以往任何时候都更具承重意义,因为我所组合的组件天生是不透明的。一个工具、一个子智能体、一次模型调用,都是一个模块:你基于一份契约去调用它,而你无法读懂它的内部。整场游戏的关键就在于那份契约是否成立——一个声称要”搜索代码库”的工具,是否真的返回了其规约所承诺的东西,又或者把一个模型换成另一个,是否悄然削弱了系统其余部分所依赖的某个后置条件。这正是穿上 2026 年衣裳的 Liskov 替换原则:一个被替换进来的组件,必须恪守它所取代的那个组件的承诺。陈述契约、并核验子类型是否恪守它,这套纪律,恰恰就是让证据门槛不只是一句口号的那套纪律——一个你可以分块推理的系统,因为每一块都说话算话。
常见问题
Barbara Liskov 的工程哲学是什么?
Liskov 的核心信念是:类型由它的行为而非它的表示来定义,而这正是让大型程序变得可驾驭的东西。一个模块就是一份契约——一组具有特定含义的操作——而契约的目的在于,你无需理解模块如何构建就能使用它。这一数据抽象的理念贯穿了她构建的一切,从 CLU 语言到 Argus 分布式系统,并孕育出她最著名的成果:子类型必须兑现父类型作出的每一个承诺这一原则。451
什么是 Liskov 替换原则?
它要求子类型能在任何期望其父类型出现的地方被使用,而不破坏调用方的假设。用 Liskov 和 Wing 1994 年的正式表述来说:”设 φ(x) 是关于类型 T 的对象 x 可证明成立的某个性质。那么对于类型 S 的对象 y,φ(y) 也应当成立,其中 S 是 T 的子类型。”1 在她 1987 年的 OOPSLA 主题演讲中,她把它表述为一条替换性质:若把一个类型 S 的对象替换为一个类型 T 的对象,能使每个程序的行为都保持不变,那么 S 就是 T 的子类型。6 在实践中,一个真正的子类型所要求的不能多于其父类型(更弱或相等的前置条件),所承诺的不能少于其父类型(更强或相等的后置条件),并且要保持父类型的不变量。那些流行的”如果它看起来像鸭子”的说法并不是 Liskov 的,也没抓住要点:这一原则讲的是恪守承诺,而非表面的相似。7
Barbara Liskov 发明了什么?
她设计并领导实现了 CLU 编程语言(始于 1973 年),它引入或推广了抽象数据类型、迭代器、结构化异常处理和参数化多态——这些特性如今已是 Java、C#、Python、Swift 等语言中的标准配置。4 更早时她构建了 Venus 分时操作系统;后来她创造了 Argus——第一门面向分布式程序的高级语言——以及 Thor——一个分布式的面向对象数据库。23 她与 Jeannette Wing 一道形式化了行为子类型,也就是如今所称的 Liskov 替换原则。1
Barbara Liskov 为何获得图灵奖?
ACM 将 2008 年的 A.M. 图灵奖授予她,”表彰其对编程语言与系统设计的实践与理论基础所作的贡献,尤其与数据抽象、容错和分布式计算相关。”8 这份认可贯穿了她的整个职业生涯:通过 CLU 让数据抽象成为一种编程语言的基本要素,推进了模块化与子类型理论,并把这些理念用到了在会各自独立故障的机器之间构建可靠系统这一难题上。她是美国最早取得计算机科学博士学位的女性之一(斯坦福,1968 年),如今是 MIT 的研究院教授。2
来源
-
Barbara H. Liskov and Jeannette M. Wing, “A Behavioral Notion of Subtyping,” ACM Transactions on Programming Languages and Systems 16, no. 6 (November 1994): 1811–1841. The Subtype Requirement: “Let φ(x) be a property provable about objects x of type T. Then φ(y) should be true for objects y of type S where S is a subtype of T.” Conditions: methods with weaker-or-equal preconditions and stronger-or-equal postconditions, preserved invariants and history properties. Publisher of record (DOI): 10.1145/197320.197383. ↩↩↩↩↩↩↩
-
“Barbara Liskov,” Wikipedia. Born November 7, 1939, Los Angeles; BA mathematics (physics minor), UC Berkeley, 1961; PhD, Stanford, 1968, advisor John McCarthy, on chess-endgame programs (killer heuristic); one of the first US women to earn a CS PhD. Venus OS at Mitre; CLU; Argus (“first high-level language to support the implementation of distributed programs,” with promise pipelining); Thor object-oriented database; MIT Institute Professor. IEEE John von Neumann Medal (2004); National Inventors Hall of Fame (2012); Benjamin Franklin Medal (2023). ↩↩↩↩↩↩↩↩↩↩↩↩↩↩↩
-
“Barbara Liskov,” Encyclopaedia Britannica. Venus time-sharing system; CLU and data abstraction; Argus distributed programming; Thor distributed object-oriented database; 2008 Turing Award. ↩↩↩↩↩↩
-
“CLU (programming language),” Wikipedia. Designed by Barbara Liskov and students at MIT, begun 1973, first appeared 1975. Clusters (the type-extension/abstract-data-type mechanism); iterators via
yieldcoroutines;signal/exceptexception handling; type-safe parameterized types (parametric polymorphism) and variant types; multiple return values. Influenced generics and iterators in Java, C#, Python, Ruby, and was credited by Swift’s designers. ↩↩↩↩↩↩↩↩↩↩ -
Barbara Liskov and Stephen Zilles, “Programming with Abstract Data Types,” Proceedings of the ACM SIGPLAN Symposium on Very High Level Languages, 1974. The foundational paper introducing the abstract-data-type approach that CLU implemented. See also Liskov’s retrospective talk “The Power of Abstraction” (OOPSLA, 2009). ↩↩↩
-
Barbara Liskov, “Keynote address – data abstraction and hierarchy,” ACM SIGPLAN Notices 23, no. 5 (May 1988): 17–34, from the OOPSLA ‘87 Addendum to the Proceedings. The original substitution property: “What is wanted here is something like the following substitution property: If for each object o1 of type S there is an object o2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o1 is substituted for o2, then S is a subtype of T.” ↩↩↩
-
“Liskov substitution principle,” Wikipedia. Origin in Liskov’s 1987 keynote and the 1994 Liskov–Wing formalization; the popular paraphrase “objects of a superclass may be replaced by objects of a subclass without breaking the program”; behavioral-subtyping conditions; the rectangle/square violation as the canonical counterexample. The “duck typing” phrasings are not Liskov’s. ↩↩↩↩
-
“Barbara Liskov – A.M. Turing Award Laureate,” ACM. 2008 Turing Award citation: “For contributions to practical and theoretical foundations of programming language and system design, especially related to data abstraction, fault tolerance, and distributed computing.” Announcement and extended citation (“data abstraction, modularity, fault tolerance, persistence, and distributed computing systems”): CRA-WP. ↩↩↩
-
Barbara Liskov, “Distributed Programming in Argus,” Communications of the ACM 31, no. 3 (March 1988): 300–312. Argus as an extension of CLU for distributed programs; guardians (objects encapsulating distributed state, accessed via handlers); atomic actions with strict consistency and atomicity guarantees coordinated by two-phase commit; nested distributed transactions. See also “Guardians and Actions: Linguistic Support for Robust, Distributed Programs” (Liskov and Scheifler, 1983). ↩