这篇来介绍一下程序语言的类型系统。部分内容是TAPL(Types And Programming Languages)的读书笔记,但不全是.
无类型Lambda演算
无类型Lambda演算其实只有两个内容：抽象(Abstract)和应用(Apply).抽象是引入Lambda表达式\(\lambda x.t\),应用是函数调用\(t \; t\).
对于无类型Lambda演算而言,其语义就是用替换完成函数调用,也就是\((\lambda x.t_1)t_2\)等于用\(t_2\)替换\(t_1\)中自由出现的所有\(x\).
基于这样的语法和语义,足以得到和图灵机等同的计算模型,例如Church数:
\[0=\lambda s.\lambda z. z, 1=\lambda s.\lambda z.s\;z, 2=\lambda s.\lambda z.s\;s\;z,\cdots\]
又例如Y组合子,可以用来构造递归函数:
\[Y=\lambda f.(\lambda x.f(\lambda y.x\;x\;y))\;(\lambda x.f(\lambda y.x\;x\;y))\]
因为\(Y\;f=f(Y\;f)\),所以也叫做不动点组合子.这个构造还是相当巧妙的.
简单类型Lambda演算
尽管利用无类型Lambda演算,足够达到完全的计算能力,但我们对无类型演算的结果是完全无知的(甚至可能发散),所以我们会希望像集合论一样引入对值的限制,在计算之前就能获得一些信息.
具体而言,我们希望引入类型\(T\),如果一个项\(t\)具有类型\(T\)那么记作\(t:T\),这往往意味着\(t\)的取值范围被\(T\)所限定.
为了适应Lambda演算,我们需要引入函数类型\(T\to T\),构成简单类型Lambda演算.此时Lambda表达式也需要引入类型:\(\lambda x:T.\;t\),函数调用不变.这样构造出的演算系统叫做简单类型Lambda演算\(\lambda_\to\).
利用Lambda表达式中标出的类型,我们足够推断出每个项的类型,这个过程和逻辑系统的推理很相似,假设前提(环境)为\(\Gamma\),那么类型推断包括三条规则,声明,抽象和应用:
\[\frac{x:T\in\Gamma}{\Gamma\vdash x:T}\] \[\frac{\Gamma,x:T_1\vdash t:T_2}{\Gamma\vdash(\lambda x:T_1.\;t):T_1\to T_2}\] \[\frac{\Gamma\vdash t_1:T_1\to T_2\quad\Gamma\vdash t_2:T_1}{\Gamma\vdash(t_1\;t_2):T_2}\]
有些项是不能根据这些推理规则推断出类型的(比如Y组合子),这样的项恰恰也是不会算出一个合法值的,这表明简单类型Lambda演算构成一个类型安全的系统.
类型推断与逻辑系统的相似性导致了Curry-Howard同构:将类型对应到命题逻辑中的命题,若存在某个项以\(T\)为类型,那么\(T\)对应的类型在直觉主义逻辑中对应真命题,否则对应假命题.这里直觉主义逻辑是不承认矛盾律/排中律的命题逻辑系统,我认为这恰恰是Curry-Howard同构的实质——构造出项的过程就是直觉主义逻辑的"构造性证明".
简单类型Lambda演算的扩展
我们可以引入记录/元组/结构体类型,也叫积类型\(T_1\times T_2\),因为它对应集合的笛卡尔积.我们可以相应地引入元组产生和消去时的类型推理规则.
我们也可以引入枚举体/(tagged) union类型,也叫和类型\(T_1+T_2\),它对应集合的无交并.我们可以相应地引入union产生和消去时的类型推理规则.
Y组合子在简单类型Lambda演算中无法表示,但我们可以特别地引入不动点算子\(\mathrm{fix}\),它作用在一个函数上就相当于能够递归计算\(\mathrm{fix}\;f=f(\mathrm{fix}\;f)\).它的类型可以表示为\(\mathrm{fix}:(T\to T)\to T\).但是,引入\(\mathrm{fix}\)会使我们很容易构造出发散的项,实质上破坏了系统的类型安全性.
我们也可以引入列表\(\mathrm{List}\;T\),这里不再详述.
类比集合中的包含关系,我们可以引入子类型的概念:如果\(S\)的任何项都可以当作\(T\)的项来使用(类型安全),那么就称\(S<:T\).在此基础上,我们会引入新的推理规则:既包括产生子类型关系的推理规则,又包括子类型作用于项上得到的推理规则.
前者会产生协变和逆变的概念:设有某个类型构造器\(F[T]\),如果\(S<:T \Rightarrow F[S]<:F[T]\)那么就是协变的,如果\(S<:T \Rightarrow F[T]<:F[S]\)那么就是逆变的.记录对它的每一项都是协变的,函数类型对参数类型是逆变的而对返回类型是协变的.
多态、Hindley Milner、System F
多态即是希望一个项可以具有多种可能的类型,但根据调用的上下文又可以确定被调用时真正的类型.简单类型Lambda演算只支持确定的类型,为了达到多态我们会引入类型变量\(\alpha\)以及全称量词\(\forall\).在这种情况下,我们的类型可以利用全称量词来构造:\(\forall\alpha\;T\),而Lambda表达式也可以引入类型变量:\(\Lambda\alpha.\;t\).例如,我们可以写出\((\Lambda\alpha.\lambda x:\alpha.\;x):\forall\alpha\;\alpha\to\alpha\).
具有这样的全称类型(universal type)的系统我们叫做System F;它也叫二阶类型系统,这是因为它对应的是二阶逻辑系统(的一部分).二阶系统允许将谓词作为全称量词的变量,一阶系统则是允许将对象作为全称量词的变量.顺便一提,一阶逻辑系统对应的类型系统是依赖于项的类型(dependent type),只有依赖类型和类型变量都存在时才能对应到完整的二阶逻辑系统.
System F本身已经是一个非常大的系统了;一个最大的特点就是System F中的类型推导是不可判定问题.由于这个缺点,实际的语言可能希望弱化System F,得到一个比较实际的类型系统,这就是Hindley Milner类型系统,它要求类型变量必须在最开始就写出来,也就是不允许\((\forall\alpha\;\alpha\to\alpha)\to T\)这样的类型.在这样的类型系统中,类型推导可以转化为给定两个带参数的类型,寻找一种对参数的取法(代换)使得两个类型相同,这就是所谓的合一.这样的类型推导算法也叫Algorithm W.
System F可以加上子类型,此时我们会希望写出\(\forall\alpha<:T\)一类的式子(叫做受限量词bounded quantifier),这样得到的类型系统叫做\(F_{<:}\).我们还可以拓展到高阶类型,将类型构造器也放到全称量词后面:具体而言,我们将确定的类型和类型变量放入同一个类,记作\(T::*\);接受一个类型得到一个类型的类型构造器则输出另一个类,记作\(F::*\to*\).在此基础上,我们可以构造出类型间的函数"类",这些类叫做类型类,对应的类型叫高阶类型,得到的系统则叫做\(F_\omega\).
最后我们以lambda cube结束这篇文章.从\(\lambda_\to\)出发,我们可以加入三种要素:依赖类型、多态(类型变量)、类型算子(类型构造器),分别得到的是LF(Logical Framework)、System F、\(\lambda_\omega\). System F加上类型算子得到的则是\(F_\omega\),再加上依赖类型则成为了CC(Calculus of Constructions).这些类型系统(加上一些未提及的类型系统)组成了一个立方体,即是lambda cube.