笔记仓库

正常人的正常笔记集

零基础开始读类型系统(Cardelli的type systems小结)

在找TAPL相关材料时,被豆瓣网友推荐先去读一下Luca Cardelli的这篇Type Systems1只有41页的小册子,当时粗略看了一下这个summary感觉很简洁易读,就放在阅读材料调查计划里差不多拖了一年没看,这两天因为一些原因找到不错的机会静下心来断断续续的读完了,观感上来说确实是让人读起来有瘾的东西,没有特别痛苦的内容,基本上是符合直觉的。对于状态良好的,有一定编程语言使用经验的,对符号逻辑有基本了解,但对编程语言类型系统没有系统性认知的人来说,原文预计需要大约一个下午的时间读完,请有相关计划的读者做好相应的规划。

我在这里粗浅的总结一下从中的收获,以及阅读中可能遇到的理解问题和解决方法。

结构概述

全文主要讨论的问题可以直接看Page 2开头部分,把每个部分的主要内容都提前交代了。

  1. Introduction: 解释了一些类型系统的基本概念名词,主要在于介绍类型系统设计的目的和几个评价标准,目前几种编程语言又是如何通过不同的实现达到相应的安全和效率目的。总之这部分可以看的稍微快一点,很综述性的东西。
  2. The language of type systems: 开始正式定义一种符号语言来描述编程语言中的类型系统,包括类型系统的基本规则,推理运算的表达,试图用这种符号语言讨论类型系统在上面提到的需要解决的问题。
  3. First-order Type Systems:用这种规范的语言开始描述第一个类型系统$F_1$,暂不探讨1st-order和2nd-order的差异,从最简单的,函数式的编程语言开始一步步定义了常见的类型,导出规则,作为后面几种类型系统的基础。
  4. First-order Type Systems for Imperative Languages:在上面的基础上引入声明和命令这些语法,并给出了它们在类型系统中的相应规则。在文章中不是很重要的内容。
  5. Second-order Type Systems:在$F_1$的基础上,开始描述一种将类型作为类型的参数构造新类型的类型系统$F_2$及新类型的相关导出规则。
  6. Subtyping: 引入子类型规则,简单的构造了在前面两种类型系统基础上实现子类关系后的$F_{1<:}$和$F_{2<:}$。
  7. Equivalence: 最简的解释了类型之间等价关系是什么,以及几个判断的例子,在文章中不是很重要的内容。
  8. Type inference:演示了在上面这些类型系统中简单的类型推断规则的使用(是的,只是最简模型的方法,甚至不能算的上是算法),提及一些现有类型推断和重构中存在的难点。
  9. Summary and Research Issues:文章常见的结论和展望部分,不多废话了,因为这篇文章比较老所以前景性的东西也没有必要认真看待,不过倒是提及了类型系统和数学的类型论(type theory)方向之间的关系,有兴趣的可以自行去nLab或者别的地方学一下类型论。

后面的术语定义表和参考文献部分没有特别新奇特别值得注意的内容,但是我建议第一次读这篇文章时,初遇其中概念,理解模糊时可以快速查一下Page 37开始的Defining Terms部分,相比正文的解释,它对概念的描述更简洁直观。当然,顺序阅读到这里时,也可以快速读一下检验自己的理解是否准确清晰。

概念&推算的理解

阅读中可能会遇到一些理解上的困难,比如Page 21-22所做的Encoding of Divergence and Recursion via Recursive Types和Encoding the Untyped $\lambda$-calculus via Recursive Types部分我也真没怎么明白,和下文也没有什么关系,就直接跳过去了。

造成这种困扰很可能是因为全文的符号公式系统都是为了简洁而作出这样的呈现,与主流的符号系统存在一些细小的差异,而篇幅所限又不可能作出过于详细的解释和说明。

所以遇到不理解的地方,可以先查文章结尾部分的Defining Terms,如果还是得不到解答,去找TAPL相关内容(符号使用上更加直观)或检索相应关键词找相关的讲义和课件。这些尝试都失败以后,不妨放心的跳过去,反正很多内容和下文的关系也没有想象的那么大。

我在这里给出一些我阅读时纠结过的东西,以及最后对它们的结论,都是比较细节的东西,不保证完全的正确性,只希望思考过程能对以后看到的这里的人有所帮助。

背景

类型系统相应的背景概念,对应Page 1-9,怎样的类型系统是安全的,编程语言的类型系统怎么分类,这些用文字阐述的东西,有相应编程经验应该不难出现理解问题。这部分如果有困难,直接按照名词去Defining Terms读最简的定义强行记忆。

值得一说的是,全文规避了一些如强弱类型这样无论在文章还是现实中都不怎么重要的概念之争,就是不希望你还浪费时间在考据这样无聊的定义上。能理解就理解,不能理解就假装自己知道了,编程经验上来了以后看这些东西都不算事。

Union Types

$F_1$的大部分基础类型没什么特别需要注意的,可能到union type开始会感觉有点陌生,前面的product type可以对应到常见的序对(pair)结构来理解,而union type如果没有相应的使用经验可能一下子想不起来。容易联想到C/C++的union structure,虽然二者有相似的地方(共有同一空间)但概念上并不是等价的东西,请忘掉它。使用过Standard ML或者Haskell就会容易理解公式系统中$A_1+A_2$这样的“加法”操作实际上等同|,用伪代码表示为

1
def type A = A1 | A2

新的类型$A$实例化后的变量可以是一个$A_1$,或者是一个$A_2$类型的变量,都可以赋值给$A$类型的变量,两种类型都是$A$的“可能性”。使用时可以通过case关键字来确定具体的类型进行不同的操作,这一点上有点类似于我们通常说的多态(事实上Standard ML也确实是把它作为多态来实现的)。

如果不去考虑$A$是通过类型来定义的,也可以类比为C/C++的enum structure,不同的是union type所“枚举”的是类型,而enum枚举的是变量值,但在使用时一个变量只会有一种类型或值,只是它是来自定义中枚举的所有可能性之一。

union type很基础,后面也常用到,所以能理解尽量还是理解一下。它也通常和product type相对出现,几乎所有类型规则也都能找到对应关系,同理它们的推广record type和variant type,包括后面子类关系规则,建议把它们对照着看方便理解。当然inLeftinRight这些构造方法定义的很模糊,不太友好,后面的用法也和这里不太一致,所以这里细节不要太深究了。

Recursive Types

虽然递归定义类型我们经常用(比如链表,二叉树)但抽象出符号语言还是一时难以习惯,毕竟之前可能没接触过$\mu$算子。

这里我个人建议可以稍微去读一下TAPL Chapter 20,或者其他材料2的文字解说和符号描述。

$\mu$算子与$\lambda$算子有相似之处。假设需要通过一个类型$X$递归构造出新的类型,可以使用函数$\lambda X.T$,$T$中出现过$X$,但$T$ 在形式上 不完全等同于$X$,如果有某个$X^*$可以使得$X^*=[\lambda X.T]X^*$这个等式(右边也可以更正式的写为$[X^*/X]T$,表示将$T$中所有出现的$X$都替换为$X^*$,相似的表达还有TAPL的$[X \mapsto X^*]T$)成立,那么这个$X^*$就是该函数的一个不动点,表示为$X^*:=\mu X.T$,当然以上只是我个人给出的不严谨的解释,一般来说直接用$\mu X.T$来表示这个recursive type来表示就可以了。

文章提到的作用于recursive type的两个操作foldunfold的定义可能有点费解,其实这也涉及上面那个不严谨的表达$X$到底和$T$是不是等价类型?如果是,能否把$T$中出现的$X$都用这个等式的(特)解$\mu X.T$替换掉?

讨论recursive type类型是否相等那一般就是说isorecursive和equi-recursive了,而那两个操作还是在讨论isorecursive,不展开更抽象的概念描述了,直接去看它们做了什么。

对于一个$\mu X.T$的unfold操作定义为把$\mu X.T$类型展开成$[\mu X.T/X]T$,即直接把不动点代入$T$展开一层,它的逆过程fold相应的把$[\mu X.T/X]T$折叠到$\mu X.T$

TAPL的替换标记稍有不同

如果还是不理解这个操作可以想想一般的Y combinator,或者直接不用这套语言体系,说一下foldunfold更广泛的使用场景:有一个函数$f$在$x$点取到$x=f(x)$即我们通常说的$x$是不动点,unfold就是把这个特定的不动点放到函数中再展开为$f(x)$,fold就是把$f(x)$折叠回$x$,上面的recursive type也是这个规则的特例。

用recursive type来描述类型的例子可以看我上面给的材料里面给出的二叉树,自然数列表,甚至自然数类型本身。回到文章中后面给出的一个用于检验理解的实例,构造list

推算检验的难点在于各类操作符的省略很严重(比如inLeftinRightfoldunfold的下标都没有标明,实际上前两者视情况构造,后两个是$List_A$,也就是第一行那个$\mu$表达式),相比文章前半部分事无巨细的导出演绎,这里开始省略了很多作者认为不重要的内容,连文字说明都没有给出,而且对我这么笨的人来说直接算fold是很困难的,所以只能想象成unfold的逆过程开始看:

把$nil_A$作为参数unfold出来,$$[nil_A/X](unit+(A\times X))=unit+(A \times nil_A)$$应该是在形式上与$nil_A$“同构”的(我前面说了不讨论isorecursive,所以这里可以简单理解为形式上等价),所以构造时选择用$InLeft\text{ }unit$构造了一个$unit+(A \times nil_A)$类型的值$unit$作为空列表。当然这里的$InLeft$应该被看作按照参数$x:X$构造出任意右半部分的构造器,构造结果可以被当成$x:X+top$,$top$为任意类型。

当然正向思考也可以说这里有一个$unit:unit+T$可以成为$X=unit+(A\times X)$的解,fold回去可以找到推断出$T$的具体类型,但这个union type其实也不怎么重要,最终结果$unit+T$一定与$List_A$同构,反正它的值也已经确定为$unit$了(这是前文关于系统中空类型的规定,我们只是试图根据规定构造的更自然一些),这个fold的结果就作为$nil_A$了。

$cons_A$前面那堆curry先不看,没什么影响,直接仿照前面正向推断看fold的参数:$\langle hd,tl \rangle:A \times list_A$被$InRight$构造成了一个$\langle hd,tl \rangle:unit+A \times list_A$,注意可以直接推断出这里union type的另一部分也就是$inRight$的下标就是$unit$按照fold规则,整个变量的类型从$unit+A \times list_A$直接折叠到了$list_A$,得到的就是$\langle hd,tl \rangle:list_A$

后面的listCase不难理解,不多说了。TAPL 20.2给出了相似的实现自然数链表NatList的例子,相对来说符号描述上更友好一些,也可以参照着它的例子来理解:

TAPL Page 278

Existential Types

$F_2$引入了“全称量词”(universally quantifier type),关于这个可以由类型来特例化的类型,原文说明的很清楚详细了,通过这样的描述可以很直观的感受到高阶的性质。

之后新引入的“存在量词”一开始接触可能有点困难,毕竟全文没有正面给出关于它的准确定义,但回过去读一遍它的例子BoolInterface可以理解pack的具体工作:

如果用类型变量$X$定义的$M:A$被用一个类型$B$可以实例化为$[B/X]M:[B/X]A$,那么我们可以存在一个$X=B$可以实现$M:A$这样的抽象,并把这一个特殊的实现用pack打包封装起来作为一个表达式,不用知道具体的实现($X=B$)只要了解有这样一个$X$类型可以让实例化后的$M$是$A$类型,这里的$M$和$A$都是一种的抽象,我们所有可以从打包后的结果看出来的只有“存在一个具体的$X$,以及一种具体的实现方法,可以实现它”,因此它的类型可以被表达为$\exists X.A$

这个思想类似于抽象接口,隐藏了类型的具体实现,来看它的例子,假设我们需要实现一个BoolInterface,这个接口实际上是一个record type,需要规定true,falsecond这些域的类型信息,但它们的类型仍然是抽象的,需要“传入”一个具体的Bool类型来实例化它们的类型,从而确定整个record的类型

这里选择把Bool类型实例化成unit+unit并给出一种实现方法,注意with后面的语句就是上文的$M$,还是以Bool为类型变量参数在构造一个record实例,当然具体的构造方法并不重要,没有细究的必要,打包结果BoolModule就是BoolInterface类的一个被实现的实例。

回到前面的Val Open假设:如果$M$是一个已经完成打包的$\exists X.A$类型的表达式,$N$是一个使用了参数:类型变量$X$和用$X$定义的$A$类型的一个实例$x$的表达式,并且$N$的最终类型为$B$(注意这个$B$和前文pack使用的$B$没有任何联系,如果这里困惑可以把$B$换成别的符号),open操作把$M$封装时用到的那个特定的$X$(也就是前文pack的$B$)和$x:A$的真正实现(前文pack的$[B/X]M:[B/X]A$)作为“实参”直接传入$N$,当然,全程你依然对这个特定的$X$一无所知,却可以使用它来计算$N$生成一个$B$类型的结果,这也是接口和模块要求的对于实现细节的遮蔽。

对于BoolModule来说,open的具体实例为

boolOp.cond(Nat)(boolOp.true)(1)(0)中,boolOp被约束到了前文with后面的那个record type的值,这个语句里面虽然没有显式的出现Bool类型,但如果出现Bool也是被约束到unit+unit来进行整个语句的求值。这个语句最后的返回结果是自然数1。

这里想明白以后后面关于existential type的意义描述也就不难理解了,不再展开多谈。关于它的定义,性质,用法可以见TAPL Chapter 24的详细叙述,以及type theory也有数学上定义的existential type,老实说,这些延伸材料关于existential type的部分我都没细看,给不出特别有效的指导建议,只是感觉和在原文里的讨论形式上差别很大。

Subtyping & Type inference

我没有任何说这两个东西不重要的意思,相反它们非常重要。只是相比前面基础概念的定义,并没有多少构造性的东西,只要前面的理解没有问题,直接往后读这两块还是非常顺利的,没有提及太深刻的东西,trivial的问题也没展开说明直接跳过了,重点在于规则的应用。

subtype关系的规则大部分是符合直觉的,比如record的长度规则,可以联想OOP的继承关系,子类比父类有更多的域;再比如variant的长度规则相反,子类所拥有的“可能性”越少,长度越低。

讨论函数类型之间的子类关系时,需要考虑它们的参数类型和返回结果类型。这里就用到了covariant和contravariant的说法,文章中倒是给出了这两个名词的解释:与整个函数类型的子类关系变化方向一致的是covariant,返回类型上就是遵循这个规则;而与函数类型的子类关系变化方向相反的就是contravariant,参数则遵循这个规定。我也曾经随手写过一个知乎想法评论给出过我的理解:

反正一句话的事
function subtyping is contravariant in arguments and covariant in results.
一个提供更多信息的函数应该输入更少信息并返回更多信息。

文中也给出了一个总结,总是出现在第奇数个箭头左边的类型是函数类型的contravariant,文章给出的例子是

1
2
X->Unit
(Unit->X)->Unit

的$X$都是整个类型的contravariant,而两次contravariant又等同于covariant所以

1
2
Unit->X
(X->Unit)->X

的$X$又是covariant

这个结论用起来可能需要注意的地方是$\to$本来就是右结合的,上面两个例子用括号规避了麻烦的讨论让例子更简单,直接从左往右数$\to$是第几个就行了,但没有括号提升优先级的时候,你就得从右往左数了。

Type inference部分也没有特别不好理解的地方,给出的所谓的几个算法虽然很抽象的概括了它需要完成的工作,但并没有涉及非常实际具体的做法,所以也没什么难点可谈,真实的type inference可能遇到的问题(比如不收敛)读原文的文字材料的叙述就能了解个大概了。

细节上可能有纠结的是$F_{2<:}$的算法Table 37没说清楚Expose操作的意义


这里Expose是寻找类型$X$在类型系统中最高的一个supertype,下面使用Expose的场景也是在函数调用$M N$和高阶类型实例化$M A$时寻找$M$的类型在系统中的最大supertype,即$M$的参数的最小subtype->返回结果的最大supertype,这样就要求实参$N$的类型只能是这个最小的类型$A$才能进行推导,这样的强制Expose保证了函数调用的安全性(其他地方的Type没有这样的强制所以不保证给出符合推断的最小类型),在符合这样的调用后才会得到与返回类型一致的结果,但这里的$B$不是那个结果,只是最模糊的一个supertype,毕竟$F_{2<:}$严格来说并不是一个完备的算法,只能小心翼翼保证产生的推断结果“没有错误”而并不完全准确。

尾声

我写的东西大部分是细节理解上的讨论,只是为了防止有同样困惑的人纠结于此浪费时间,并不能取代文章本身的阅读。类型系统是计算机科学最优雅美丽的东西之一,精彩的论述还需要认真通读全文。

祝你早日找到住在计算机内的神灵。


  1. 1.Cardelli, Luca. "Type systems." ACM Computing Surveys 28.1 (1996): 263-264.
  2. 2.https://www.cs.cornell.edu/courses/cs4110/2012fa/lectures/lecture27.pdf