How Gradual Typing System Helps Us

Liyi, from Huawei, inc. 2012 Lab, OS Kernel Lab, working as

verification engineer, and
verification tool developer

Hiring @Beijing @Shanghai

写给不想看完全文的同仁们，以下是本文核心观点：

类型系统的本质是提供信息，这些信息不仅仅是提供给编译器看的，也是提供给人看的
站在工程视角，强大的类型系统并非银弹
- 强大的类型系统带来更高的开发门槛，更低的迭代速度和原型 demo 的能力（个人观点，可探讨）
- 过弱的/缺失类型系统支撑将极大降低开发质量和可维护性
没有完美的类型系统（和语言），只有最适合的
站在我们的场景下，Python 的渐进类型系统就是一个比较合适的类型系统
- 我们很喜欢 Trait (Rust/Haskell)，所以我们把 Trait 移植到了 Python

视频回顾在此：

渐进式类型系统如何帮助我们，以及如何在工程中改造Python渐进的类型系统

以下正文。

对于一个普通的开发者，类型对我们意味着什么？

一句话归纳：我认为类型是附着于程序之上的额外信息。类型系统的表达能力高低，则意味着通过类型能够提供给我们的信息的多少。高级的类型系统如精化类型系统，依赖类型系统等能够提供很多重要信息。但是这也会付出代价：类型检查变得更为困难。

今天想和大家一起聊一下，渐进式类型系统在我们的工程开发中是怎么样对我们产生帮助的，以及我们在工程实践中是怎么对 Python 的渐进式类型系统进行改造的。

我们先从一个小例子开始。在操作系统中，会有很多数据结构，这些数据结构是与 CPU 的核相关的，比如每个核的状态，每个核上在跑什么样的任务等等。这个时候每一个核有一个序号，我们称它是这个核的 id。id 的值的合法范围取决于硬件体系结构。假设我们有一个 8 核的 CPU，那这个核的号数应该在 0~7 内，即从 0 号核到 7 号核。当然，这个数字还得是一个整数。那么，当我们想要定义一个数据结构来描述这样一个 id 时，我们就需要有一个类型。

在这里插入图片描述

以 C 语言为例，最简单粗暴的定义方式，CoreID 实际上就是一个普通的整数。

// 1st definition
// It is a number ...
typedef int CoreID;

但是，CoreID 其实仅需要满足 0~7 这个范围，远小于 int 能够表示的内容，这时我们会认为这样定义的类型有点浪费。进一步地，我们可以把 CoreID 定义成一个 unsigned char，即一个无符号的 8 位整数。这样，CoreID 的范围就可以很小，同时其保存的整数是非负的（可见在这个过程中，我们增加了这个类型所抱有的信息量）。

// 2nd definition
// Small, and not negative
typedef unsigned char CoreID;

但是，我觉得这个定义还不够精确，我想要进一步细化一下 CoreID，这时我们就可以引入 Refinement Type。如有兴趣可以阅读这篇精化类型简介。

$R e f i n e m e n t T y p e s = T y p e s + P r e d i c a t e s$

下面这段代码就是 LiquidHaskell ¹ (a Refinement Type Checker for Haskell) 里 Refinement Type 定义方式。我们将 CoreID 定义为一个集合，集合的基本类型是一个整数（Int），集合里的每个元素都要在 0~7 范围内。

-- 3rd definition
-- and, satisfies a certain constraint
type CoreID = {v: Int | 0 <= v && v <= 7}

现在我们有了三种不同的类型定义。这些不同的定义方法对工程上来说有什么意义呢？

我们看下面这段代码。假设有一个数组 taskList，我们需要从这个数组中根据 coreId 取出一个数据。例如下面这样一个函数：

Task getTask(Task taskList[8], CoreID coreId) {
  ...
  return currTask[coreId];
}

大家可以看到，带了 refinement 的类型系统是可以分析出是合法的，而前两种类型定义都是不可以的。这是因为 Refinement Type 带给了我们更多的信息。

如下图所示，我们现在从更底层的角度去想。第一种定义的类型 int 在内存中占用了 32 bits（当然有可能在你的编译器里面是 64 bits），这其中有一个位是符号位，因此实际上能够用来描述的就是 31 个数据位（或者 63 个数据位）和一个符号位。

第二种定义中的类型 unsigned char 告诉我们，这个类型在内存中，实际上占用了 8 bits，而且都是数据位。

第三种类型定义能够告诉我们什么信息？其实什么信息都没有告诉我们，因为它只是定义了一个抽象的 Int。而且我们在绝大多数情况下，都不会关心 Haskell 的类型在内存里占了多少。

在这里插入图片描述

大家可以看到，这几种不同的类型定义，其实会体现不一样的信息，这些信息也未必会有一个包含关系。因此，从工程的视角去看类型系统，其核心就在于 提供信息。类型系统提供的信息可以是给 程序员 的，也可以是给 编译器 的。

在这里插入图片描述

类型系统提供的信息可以用来辅助检查我们程序的错误。换句话说，如果给一个 CoreID 赋值的时候不符合它的类型系统约束，那么类型检查工具就可以告诉我们这里可能使用了一个非法的 CPU 核。正如下图所示。

在这里插入图片描述

类型系统的重要性不言而喻

对编译器而言

进一步展开刚才的话题。类型系统可以给编译器提供信息：

类型系统可以让编译器能够检查出更多的问题，减少程序在运行中的错误。 Rust 就是一个很好的例子，它有一个强大的类型系统，可以很大程度上规避掉一些常见的内存安全问题。

类型系统还可以带给程序员更好的抽象机制。 比如 Haskell 和 OCaml 的函子（Functors）和模块（Modules），C++ 和 Java 中的泛型（Generic Types）。

类型系统还可以带给我们更好的性能。 当编译器能够推导出更多的东西，我们就可以在编译期做更多的优化。这其实是我们更看重的作用。

对开发者而言

从工程的角度来说，我们在很大程度上还看重类型系统给程序员（或者开发者）所提供的信息，这些信息也表现在两个层面

类型系统对于代码的可读性和可维护性的提升。

但并不总是这样的。大家可以看下面这段从 Coq（一个非常著名的证明系统，用 OCaml 实现）里截取的代码。类型系统还有一个很大的作用，就是提供类型的自动推导功能，让程序员可以少写很多参数。但大家在看到这段代码时，是很难一眼看懂这个程序到底写了什么，因为所有的变量都没有任何的类型，如果没有更大的上下文，那我们就不知道这个程序到底想要干什么。

...
and mimick_undefined_evar evd flags hdc nargs sp =
  let ev = Evd.find_undefined evd sp in
  let sp_env = reset_with_named_context (evar_filtered_hyps ev) env in
  let (evd', c) = applyHead sp_env evd nargs hdc in
  let (evd'',mc,ec) =
    unify_0 sp_env evd' CUMUL flags
      (get_type_of sp_env evd' c) ev.evar_concl in
  let evd'''= w_merge_rec evd'' mc ec [] in
  if evd'== evd'''
  then Evd.define sp c evd'''
  else Evd.define sp (Evarutil.nf_evar evd'''c) evd''' in

另外，类型系统在团队协作时还可以作为一个交流的接口而存在。 当我们看到其他人定义的类型和接口封装时，我们其实可以大体理解这个程序要做什么，所以我们可以不用去过分关注类型内部具体的实现。

如何定义一个好的类型系统

前面所讲的类型系统的作用，可以归结到很多个优点，包括可靠性，开发效率，性能，以及团队协作等。

在这里插入图片描述

但是，天下没有免费的午餐，类型系统也没有十全十美的设计。当我们去设计一个类型系统的时候，会有包括 表达能力 Expressiveness，可判定性 Decidable，用户易用程度 User-Fridenly 等多方面的考虑。

比如 C 和 Go 语言，用户用起来不是很困难，但是其表达能力相应地也比较弱。而像 Coq 和 RefinedC ² 发表在 PLDI 2021，官网：https://plv.mpi-sws.org/refinedc/），虽然表达能力很强，但它是不可判定的。Haskell 和 Rust 的表达能力很强，同时也是可判定的，但它对用户或者说对大多数人来说不是特别友好。

在这里插入图片描述

所以，类型系统是否足够好，或者说是否适合我们使用，其实有多个判断维度。作为一个开发者，我总是希望在我自己的场景里，能够有一个合乎这个场景的类型系统，即能够在这三个方面找到平衡。包括 refinement type 也是，到底在什么场景下，对我们的帮助是最大的，最合乎时宜的。

但是，这个问题没有答案，因为这个问题是非常领域特定的。接下来，我会给大家分享一个我们实际的例子，即在某一个项目开发场景中，我们是如何使用以及定制 Python 类型系统的。

Python 类型系统

接下来，进入到今天分享的第二部分，一个既不 sound 也不 complete 的 Python 类型系统，以及我们是如何将它应用到一个大型项目中？

在这里插入图片描述

知乎上有这样一个问题，很多人认为在大型项目上，Python 并不是一个很好的语言，但我个人认为这是一个值得商榷的问题。

在这里插入图片描述

项目背景

我有一个真实的项目是做一个形式化验证工具，这个工具要对上层的 C/C++ 实现内核、驱动或者一些库。我们需要将其变成一个中间层的验证语言，基于这个语言去做很多不同的分析。

这个项目里包含三部分，第一部分是 语言前端。第二部分是 核心的框架，这部分会包含一个中间语言的实现（IVL）以及很多的分析工具，比如抽象解释，符号执行，代码自动生成，指针分析等。我们团队会基于这个框架去支撑各种的软件验证，包括一些 domain-specific 的静态分析，锁的分析，调用图分析，还有模型驱动设计、代码编译测试等很多不同的场景。

在这里插入图片描述

现在，我们需要关注中间这一层。中间这层需要有很多人协作，并且会提供给不同的领域做二次开发。这层框架的特点是：

不稳定 因为我们在持续开发。
对性能不敏感 不管是 SMT 求解器还是程序分析，这些工具本身都是特别重量级的。对于工具之上的这层框架（或者一个胶水语言）来说，它的性能到底好不好，其实并不是特别的敏感。
可靠性 在这个项目场景下，我们还非常关注框架的可靠性。作为一个形式化验证的工具，可靠性当然是必须的。

Python 的类型系统

因此，在这个大前提下，我们项目选择了 Python 作为框架的开发语言，因为 Python 生态比较好，开发起来比较快。具体原因这里就不展开讲了。

我们希望 Python 本身也要有很高的可靠性。

这个可能与大家日常理解的 Python 作为一个原型语言的开发模式有一定的违背，因此，我们利用了 Python 本身的类型系统。可能很多人不是特别的了解，Python 本身支持了 渐进式的类型系统 Gradual Typing ³，它允许我们一部分一部分地往程序里添加一些信息息。

具体原理是这样的，每一个程序里，除了原本描述程序行为的部分，还包括一些类型标注。这里的类型标注就与我们在 C/Haskell/Ocaml 中所写的类型声明并无二致。而不同的是，Python 的类型标注不会在执行环境中体现，等于说这个类型系统是没有语义。 但是它会有一个工具将这个类型系统单独抽出来，交给类型检查器（Type Checker）里去进行检查。之后我们根据检查结果对源代码进行修改。

那么，我们就可以先写一个不带类型标注的程序，编译运行成功后，再慢慢地将类型添加到代码中，将代码里很多的 corner case 通过工具检查来干掉。

在这里插入图片描述

所以，这样的一个类型系统会有什么样的特点呢？

首先，这个类型系统 对性能没有提升，因为它根本就不带入运行时。
其次，我们的 开发过程与类型标注（或者说类型的开发） 可以是完全拆分开来进行。
这个类型系统本身的 演进可以特别快。类型系统语义，和编程语言的执行语义是两件事情。所以类型系统的特性跟编程语言的特性互不影响，可以分别进行迭代。

Python 类型系统演进

给大家简单介绍一下我们所看到的 Python 类型系统的演进过程。（部分总结来自于知乎用户 @Manjusaka）

Python 最早的类型系统的标注是在 PEP 3107 —— 函数注解 ⁴ 里提出的，以冒号 : 的形式给函数参数添加类型注释。但是 Python 编译器并未增加类型检查，若类型使用错误，编译器也不会报错，我们甚至可以将下面代码中参数 a 的类型标注为一个字符串。（你可以通过 mypy 库来检验最终代码是否符合注解。）
在这里插入图片描述
后来 PEP 484 – 类型提示 ⁵ 和 PEP 526 – 变量注解语法 ⁶，Python 的类型有了语义，我们可以对类型进行检查，也可以对函数里的变量进行标注。

PEP 557 – 数据类 ⁷ 和 PEP 563 —— 推迟评估评类型注释 ⁸ 之后，Python 引入了数据类的概念（@dataclass），使得我们看到的这个 Python 的类，更接近于类似 C++/Java 等强类型语言的类型系统。同时 Python 也开始支持 recursive 的类型声明，即我们可以定义了一个链表类 LinkedList，这个链表类可以同时指向自己。

在这里插入图片描述

以上的这部分，从 PEP 3107 到 PEP 563 这部分的内容，基本上就是我们现在开发中主要会使用的东西。同时，如前面所提，Python 有一个渐进能力特别强的类型系统。

比如，在 PEP 593 – 灵活的函数和变量注解 ⁹ 里引入了类型注解，即 Python 允许我们为类型指定一个谓词，比如下面代码中的 T1 作为一个整数，其范围可以是 -10~5。Python 自此开始引入了 refinement type 的概念。
在这里插入图片描述
到 PEP 647 – 用户自定义的类型保护 ¹⁰ ，Python 甚至引入了所谓的 type guards，即一个变量是不是属于一个类型，不仅可以由类型检查器来判定，甚至还可以由用户自己定义的一个类型或者函数来进行判定。这等于是由 Python 官方提供了一种可编程的类型系统，允许由开发者来自行对其改造。

在这里插入图片描述

Python 的类型系统演进，可以映射回刚才我们提到的三个概念。一是 Python 的类型系统对用户特别友好，因为它用起来很简单，可改造性非常强。此外，Python 表达能力也非常强。但是这个类型系统完全不 decidable，因为当你使用了这种非常高级的类型特性后，很多时候需要添加一些奇怪的类型声明或者类型推导的 hint，来告诉系统你这个类型是成立的。这是该类型系统的显著缺点。

渐进类型系统

但是瑕不掩瑜，对吧？当我们有了这些类型系统的特性之后，我们可以让一个 Python 的程序变成如下这样（这段代码是我刚接触 Python 时，当我需要写一个图时，我会这么写）。

class Graph:
  def __init__(self, vertexes, edges):
    self.vertexes = vertexes
    self.edges = edges

下面这段代码是我们现在团队开发的 Python 程序里，当我去写一个图的时候，我是这么去写的。首先，我们定义了一个类型变量 T（这个类型变量可以认为与 OCaml 里的 t'-> Graph.t' 这样的参数化类型）。Graph 本身可以是一个 Generic[T]，即可以接受任何类型的 T 作为它的节点，但这个节点必须要是 Hashable 的。这时，我们就可以为图里的节点和边去做如下这样的类型标注，这时候 T 就变成了一个可以在很多场景下复用，并且可以去做类型检查的类型。

T = TypeVar('T', bound=Hashable)

@dataclass
class Graph(Generic[T]):
  vertexes: List[T]
  edges: Dict[T, List[T]]

那么，为什么我很喜欢这个渐进类型系统呢？这有一个非常工程的原因。下面三个图表示了当我们面对三种不同的类型系统下的开发状态。

这个图就是在一个原始的 Python 里，即真正的弱类型系统里（或者说没有编译时的弱类型系统里），我们去做开发时，往往能够非常快就写出一个原型，但这个原型可能需要特别久的时间才能到达稳定，即真正能够交付的点。在这个过程中，我们需要反复迭代，添加各种测试和代码 review 来确保它的可靠性。

在这里插入图片描述

下图就是现在我们在使用 Rust 或者 Haskell 这类语言开发时的开发状态。我们可能需要花很长时间才能让开发的原型类型检查都编译通过（前提是不用 unsafe）。但当我们一旦有了编译通过的原型后，我们距离稳定可交付，就是一件很快的事情了。

在这里插入图片描述

当我们在用渐进类型系统的时候，这个过程会是，我们很快开发出一个原型，给原型加类型标注，在类型标注中排除各种 corner cases 的错误。并且我们可以在一个相对可控的时间里获得一个比较稳定的版本。

在这里插入图片描述

使用 Trait 提高协作

在前面的基础上，我们的类型系统相对可靠了，开发效率也比较高。但其实还有一个问题没有搞定（当然，在我们的场景下，类型系统的性能可以不关注），就是并不方便进行协作。

Reliability
Dev Efficiency
Performance ($￥)
Collaboration

下面我们以一个场景来说明。假如现在有一个团队来开发库 A，另外一个团队想要使用库 A 并进行扩充。出于很多原因，第一个团队可能并不希望对 A 的扩充直接进入到开发主线（比如这些扩充包含了领域特定的内容）。

在这里插入图片描述

这个时候，我们可以看到有很多语言的类型系统，有他们自己的解决方案。

比如说在 JavaScript 里，我们可以直接通过修改一个类的 prototype 给这个类注入一些特性。

function Person(name) {
  this.name = name
}

p = Person("foo")

Person.prototype.sayhi = function (this) { console.log(this.name) }
p.sayhi() // foo

Rust 有一个 trait 和 impl 的语法特性。trait 我们可以理解为是一种特性，我们可以在另外一个库中以非侵入式的的方式，给已经定义好的类型添加新的特性（如下面代码中通过 trait 给 Person 类型新增 sayhi() 的特性），并且（通过 impl）提供实现。这个过程完全不会影响原有库的代码。

pub struct Dog {pub nickname: String,}

pub trait Person {
  fn sayhi(&self);
}

impl Person for Dog {
  fn sayhi(&self) { println!("{}\n", self.nickname) }
}

在我看来，Rust 的 trait 和 impl 是特别优雅的语法特性，所以我们想把 trait 引入到 Python 里实现。

在 Python 里实现 Trait

我们实际上做了什么呢？

首先结果如下面代码所示，我们在第一个包里（package A）定义了一个抽象的类型 Animal，这个类型实现了一个东西叫做 TraitHub，这意味着我们可以通过 TraitHub 对 class Animal 进行扩充。

然后在第二个包里（package B），定义一个 trait 叫做 Person，这个 trait 可以 sayhi()（你可以将其理解为 Java 或者 Go 的一个接口，或者 Rust 里的一个 trait）。我们把这个 trait 再通过 class DogIsPerson 来实现。

# package A
class Animal(TraitHub):
  pass

@dataclass
class Dog(Animal):
  nickname: str


# package B
class Person(Trait):
  def sayhi(self):
    pass

class DogIsPerson(Dog, Person):
  def sayhi(self):
    print(self.nickname)

在这个过程中，作为一个程序员，我们看到的是如下这样的类图。我们有一个 DogIsPerson 类，同时实现了 Dog 和 Person。那么我们的预期是希望 DogIsPerson 类可以将它的特性注入回 Dog 类中。

在这里插入图片描述

作为 Python 的执行环境，看到的是如下的类图。通过这个 trait（我们实现为一个插件的形式）我们可以把 Dog 类反馈去寻找 DogIsPerson 类，并且把方法动态地从 DogIsPerson 里拷贝到 Dog 类中。那么，此时 Dog 类也拥有了 sayhi() 的方法。狗会说话了。

在这里插入图片描述

到此为止，我们还是没法做类型检查，因为这段代码确实可以跑，但是一旦调用这个方法时，类型检查系统就会告诉我们没有这个方法。因此，我们还去开发了类型系统的扩充，即一个类型检查器插件，这个插件能够看到 Dog 类型是 DogIsPerson 的一个子类。当然这在实际上是不存在的，这是我们插件做的一个 cheat，我们欺骗了他的类型检查器，告诉他说 Dog 是 DogIsPerson 的一个子类，从而让类型检查器能够观察到 sayhi() 这个方法，那么类型检查就不会报错。

在这里插入图片描述

这表示，我们仍然可以将整个工具无损地集成到 Python 类型检查的流程中，而且不需要特地屏蔽一些特例。我们将这个功能实现为一个 mypy 插件和 Python 运行时的一部分，并且没有对 Python 自己的 interpreter 做任何的修改。

基于此，我们成功地达成了无侵入式对 Python 类型系统的修改，最后使得我们在协作这一项上也补齐了，我们在自己项目的场景里，将 Python 的类型系统改造成了同时符合下面的三个特性。当然我们不关心性能，没有银弹，我们也牺牲了很多东西。

Reliability
Dev Efficiency
Performance ($￥)
Collaboration

写在最后

综上，我认为，类型系统其实与领域有非常强的绑定关系，如果我们的类型系统能够能够在某一些领域里面产生很好的效果，那这个类型系统就可能会有一个很大的成功。

以上就是我的分享，欢迎大家一起交流。

参考

LiquidHaskell https://ucsd-progsys.github.io/liquidhaskell-blog ↩︎
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2021). Association for Computing Machinery, New York, NY, USA, 158–174. DOI: https://doi.org/10.1145/3453483.3454036 ↩︎
Gradual Typing - Wikipedia https://en.wikipedia.org/wiki/Gradual_typing ↩︎
PEP 3107 – Function Annotations https://www.python.org/dev/peps/pep-3107/ ↩︎
PEP 484 – Type Hints https://www.python.org/dev/peps/pep-0484/ ↩︎
PEP 526 – Syntax for Variable Annotations https://www.python.org/dev/peps/pep-0526/ ↩︎
PEP 557 —— Data Classes https://www.python.org/dev/peps/pep-0557/ ↩︎
PEP 563 – Postponed Evaluation of Annotations https://www.python.org/dev/peps/pep-0563/ ↩︎
PEP 593 – Flexible function and variable annotations https://www.python.org/dev/peps/pep-0593/ ↩︎
PEP 647 – User-Defined Type Guards https://www.python.org/dev/peps/pep-0647/ ↩︎