类型系统简介

Question

类型系统是编程语言的重要组成部分，本文是对 type system 的阅读笔记和梗概，强烈推荐感兴趣的同学阅读文章本身。

类型系统的目的

类型系统(type system)的基本目标是防止程序在运行时发生类型错误。当且仅当语言运行时不存在任何形式的类型错误，那么它就是sound的。soundness 是类型系统研究的重要目标。

对类型系统的描述

描述类型系统使用的是一种符号系统，它来自于自然推演(Natural Deduction)。有如下几个组成部分：

Judgments

Judgement 是一条断言，一般具有如下形式:

\[\Gamma \vdash \Im\]

\(\Gamma\) 表示已知的事实，\(\vdash\) 表示推导出，\(\Im\) 表示推导的结果，类型断言一般用来表示变量具有指定类型。例如：

\[\Gamma \vdash M:A\]

表示在类型环境$$中，自由变量 M 具有类型 A。

有一条常用的通用断言：

\[\Gamma \vdash \diamond\]

表示类型环境\(\Gamma\)是行为良好(well formed)的。

还有一种语义：\(\Gamma,\ \Gamma' \vdash e\),这表示了已知环境\(\Gamma\)加上一个本地环境\(\Gamma'\)，可以推导出\(e\)。

Type rules

类型规则通过一条或多条断言来决定一条断言的正确性，一般有如下形式：

\[\frac{\begin{gather} (Rule\ name)\ \ (Annotations) \\ \Gamma_1 \vdash \Im_1 … \Gamma_n \vdash \Im_n\ (Annotations) \end{gather} }{\Gamma \vdash \Im}\]

横线上方是一条或多条判断，描述了规则的前提(premise)。下方只能有一个判断，描述了规则的结论(conclusion)。顶部可以标注规则的名称和注释。前提的右边也可以写一些注释。

我们来举个例子：

\[\frac {\begin{gather} (Val\ n)\ \ (n = 0,\ 1,\ …) \\ \Gamma \vdash \diamond \end{gather} }{\Gamma \vdash n:Nat}\ \ \ \frac {\begin{gather} (Val\ +) \\ \Gamma \vdash M:Nat\ \ \ \Gamma \vdash N:Nat \end{gather} } {\Gamma \vdash M+N:Nat}\]

这个例子认为在一个行为良好的类型环境中，所有的自然数都有类型 Nat，两个类型同为 Nat 的表达式 M 和 N 相加的结果也为一个自然数。

有一条基本规则：空的环境是类型良好的，不需要任何假设：

\[\frac{\begin{gather} (Env\ \varnothing)\\ \ \end{gather} }{\varnothing \vdash \diamond}\]

一系列类型规则组成的集合称为一个正式的类型系统。

Type derivations

类型导出(Type derivations)在一个给定的类型系统中，是一颗树，它的底部的根节点和顶部的叶节点都是类型断言，且每条断言都可以由它上方的断言结合烈性系统的规则直接获得。给定一个类型断言，我们可以将它放置在类型导出的根部（底部），利用类型规则一步一步向上推导，如果能够顺利推出，说明断言是合法的。

例如根据我们此前的规则，可以判断\(\varnothing \vdash 1+2:Nat\)是否合法：

\[\frac{ \frac{}{\frac{\varnothing \vdash \diamond}{\varnothing \vdash 1:Nat}} \ \ \frac{}{\frac{\varnothing \vdash \diamond}{\varnothing \vdash 2:Nat}} }{\varnothing \vdash 1 + 2: Nat}\]

Type inference

给定一个项 M，如果它在类型环境\(\Gamma\)中是类型良好的(well typed)，那么存在一个类型 A 可以赋给 M。通过类型导出为 M 确定 A，称为类型推导(Type inference)。

基础构成

语法

一阶类型的\(\lambda\)演算(first-order typed \(\lambda\)-calculus)被称作 System \(F_1\)。我们可以给\(\lambda\)演算添加类型注释，它的语法如下：

\[\begin{align} A, B &::=\ types \\ &K\ \ \ \ K \in Basic &basic\ types \\ &A \rightarrow B &function\ types \\ M,N &::=\ terms \\ &x &variable \\ &\lambda x:A.M &function \\ &M N &application \end{align}\]

断言

对于\(F_1\)我们只需要三条简单的断言：

\[\begin{align} &\Gamma \vdash \diamond\\ &\Gamma \vdash A \\ &\Gamma \vdash M:A \end{align}\]

规则

有了这三条断言，我们可以写出它的类型规则：

\[\begin{align} &\frac{\begin{gather} (Env\ \varnothing)\\ \ \end{gather} }{\varnothing \vdash \diamond} \ \ \ \ \frac{\begin{gather} (Env\ x)\\ \Gamma \vdash A\ \ \ \ x \notin dom(\Gamma) \end{gather} }{\Gamma,\ x:A \vdash \diamond} \\ \\ &\frac{\begin{gather} (Type\ Const)\\ \Gamma \vdash \diamond\ \ \ \ K \in Basic \end{gather} }{\Gamma \vdash K}\ \ \ \ \frac{\begin{gather} (Type\ Arrow)\\ \Gamma \vdash A\ \ \ \ \Gamma \vdash B \end{gather} }{\Gamma \vdash A \rightarrow B} \\ \\ &\frac{\begin{gather} (Val\ x)\\ \Gamma',\ x:A,\ \Gamma'' \vdash \diamond \end{gather} }{\Gamma',\ x:A,\ \Gamma'' \vdash x:A}\ \ \ \ \frac{\begin{gather} (Val\ Fun)\\ \Gamma,\ x:A \vdash M:B \end{gather} }{\Gamma \vdash \lambda x:A.M:A \rightarrow B}\ \ \ \ \frac{\begin{gather} (Val\ Appl)\\ \Gamma \vdash M:A \rightarrow B\ \ \ \ \Gamma \vdash N:A \end{gather} }{\Gamma \vdash M N:B} \end{align}\]

基础类型

我们有了 System \(F_1\)的基础骨架后，就可以给它增加一些基础类型。

Unit Type

Unit Type 很常见，在很多语言中它又叫 Void 或 Null 。

\[\frac {\begin{gather} (Type\ Unit) \\ \Gamma \vdash \diamond \end{gather} }{\Gamma \vdash Unit}\ \ \ \frac {\begin{gather} (Val\ Unit) \\ \Gamma \vdash \diamond \end{gather} } {\Gamma \vdash unit:Unit}\]

Bool Type

Bool Type 也很常见，它是布尔值的类型，它一般拥有一个有用的操作，即通常语言中的 if else 语句，我们在这里称为 cond :

\[\frac {\begin{gather} (Type\ Bool) \\ \Gamma \vdash \diamond \end{gather} }{\Gamma \vdash Bool} \ \ \ \ \frac {\begin{gather} (Val\ True) \\ \Gamma \vdash \diamond \end{gather} } {\Gamma \vdash true:Bool} \ \ \ \ \frac {\begin{gather} (Val\ False) \\ \Gamma \vdash \diamond \end{gather} } {\Gamma \vdash false:Bool} \\ \\ \frac {\begin{gather} (Val\ Cond) \\ \Gamma \vdash M:Bool \ \ \ \ \Gamma \vdash N_1:A \ \ \ \ \Gamma \vdash N_2:A \end{gather} } {\Gamma \vdash (if_A\ M\ then\ N_1\ else\ N_2):A}\]

在 Cond 中我们需要通过下标 A 来告诉类型检查器，结果应该是类型 A，来消除潜在的类型检查困难。

Nat Type

Nat Type 就是自然数的类型。假设我们有 0 和 Succ ，则 1 为 Succ 0 ，2 为 Succ Succ 0 。Nat 还存在两种计算： pred 和 isZero ，前者用来得到当前自然数前一位的自然数，后者用来判断自然数是否为 0.

\[\frac {\begin{gather} (Type\ Nat) \\ \Gamma \vdash \diamond \end{gather} }{\Gamma \vdash Nat} \ \ \ \ \frac {\begin{gather} (Val\ Zero) \\ \Gamma \vdash \diamond \end{gather} } {\Gamma \vdash 0:Nat} \ \ \ \ \frac {\begin{gather} (Val\ Succ) \\ \Gamma \vdash M:Nat \end{gather} } {\Gamma \vdash succ\ M:Nat} \\ \\ \frac {\begin{gather} (Val\ Pred) \\ \Gamma \vdash M:Nat \end{gather} } {\Gamma \vdash pred\ M:Nat}\ \ \ \ \frac {\begin{gather} (Val\ IsZero) \\ \Gamma \vdash M:Nat \end{gather} } {\Gamma \vdash isZero\ M:Bool}\]

结构类型

Product Types

Product Types 是一对类型，由两个类型构成，例如\(A_1 \times A_2\)就是一个 product type。这两个类型可以通过 first 和 second 操作符来提取出来。通过 with 语句，我们可以把 product type 解构为两个单独的变量\(x_1\)和\(x_2\)，应用在作用域 N 中。

\[\begin{align} &\frac{\begin{gather} (Type\ Product)\\ \Gamma \vdash A_1\ \ \ \ \Gamma \vdash A_2 \end{gather} }{\Gamma \vdash A_1 \times A_2}\ \ \ \ \frac{\begin{gather} (Val\ Pair)\\ \Gamma \vdash M_1:A_1\ \ \ \ \Gamma \vdash M_2:A_2 \end{gather} }{\Gamma \vdash \langle M1,M2 \rangle: A_1 \times A_2} \\ \\ &\frac{\begin{gather} (Val\ First)\\ \Gamma \vdash M:A_1 \times A_2 \end{gather} }{\Gamma \vdash first\ M:A_1}\ \ \ \ \frac{\begin{gather} (Val\ Second)\\ \Gamma \vdash M:A_1 \times A_2 \end{gather} }{\Gamma \vdash second\ M:A_2} \\ \\ &\frac{\begin{gather} (Val\ With)\\ \Gamma \vdash M:A_1 \times A_2\ \ \ \ \Gamma,\ x_1:A_1,\ x_2:A_2 \vdash N:B \end{gather} }{\Gamma \vdash (with (x_1:A_1, x_2:A_2) := M\ do\ N):B} \end{align}\]

Union Types

Union Types 指的是结合类型。例如一个 union type\(A_1+A_2\)可以认为是一个带有 left 标记的类型为\(A_1\)的元素或带有 right 的类型为\(A_2\)的元素。这一标记可以由 isLeft 和 isRight 来进行测试，相应的类型可以由 asLeft 或 asRight 来提取。和之前 Bool Type 的 Cond 语句类似， asLeft 和 asRight 也需要下标来帮助类型检查器进行判断。

\[\begin{align} &\frac {\begin{gather} (Type\ Union) \\ \Gamma \vdash A_1 \ \ \ \ \Gamma \vdash A_2 \end{gather} }{\Gamma \vdash A_1 + A_2} \ \ \ \ \frac {\begin{gather} (Val\ inLeft) \\ \Gamma \vdash M_1:A_1 \ \ \ \ \Gamma \vdash A_2 \end{gather} }{\Gamma \vdash inLeft_{A_2} M_1:A_1 + A_2} \ \ \ \ \frac {\begin{gather} (Val\ inRight) \\ \Gamma \vdash A_1 \ \ \ \ \Gamma \vdash M_2:A_2 \end{gather} }{\Gamma \vdash inRight_{A_1} M_2:A_1 + A_2} \\ \\ &\frac {\begin{gather} (Val\ isLeft) \\ \Gamma \vdash M:A_1+A_2 \end{gather} }{\Gamma \vdash isLeft\ M:Bool} \ \ \ \ \frac {\begin{gather} (Val\ isRight) \\ \Gamma \vdash M:A_1+A_2 \end{gather} }{\Gamma \vdash isRight\ M:Bool} \\ \\ &\frac {\begin{gather} (Val\ asLeft) \\ \Gamma \vdash M:A_1+A_2 \end{gather} }{\Gamma \vdash asLeft\ M:A_1} \ \ \ \ \frac {\begin{gather} (Val\ asLeft) \\ \Gamma \vdash M:A_1+A_2 \end{gather} }{\Gamma \vdash asRight\ M:A_2} \\ \\ &\frac {\begin{gather} (Val\ Case) \\ \Gamma \vdash M:A_1+A_2 \ \ \ \ \Gamma,\ x_1:A_1 \vdash N_1:B \ \ \ \ \Gamma,\ x_2:A_2 \vdash N_2:B \end{gather} }{\Gamma \vdash (case_B M\ of\ x_1:A_1\ then\ N_1\ |\ x_2:A_2\ then\ N_2):B} \end{align}\]

如果 asRight 被错误的应用在了由 isLeft 标记的元素上，那么我们就得到了一个被捕获的异常，这个异常不属于 forbidden error。因此有了 union Type，我们可以定义一个典型的被捕获的错误类型：

\[error_A = asRight(inLeft_A(unit)):A\]

我们可以用它来表示任何类型的异常。

Record Types

Record Types 是 product types 的升级版，它由 product types 迭代而来。对于 record M 中的每个组成变量\(x_1 … x_2\)，都有名称\(l_1 … l_2\)和它绑定。与 product types 相似，record types 也有 with 语句。Product types \(A_1 \times A_2\)在 record types 中可以定义为\(Record(first: A_1, second: A_2)\)。

\[\begin{align} &\frac {\begin{gather} (Type\ Record)\ \ \ \ (l_i distinct) \\ \Gamma \vdash A_1 … \Gamma \vdash A_n \end{gather}} {\Gamma \vdash Record(l_1:A_1, …, l_n:A_n)} \ \ \ \ \frac {\begin{gather} (Val Record)\ \ \ \ (l_i distinct) \\ \Gamma \vdash M_1:A_1 … \Gamma \vdash M_n:A_n \end{gather}} {\Gamma \vdash record(l_1=M_1,…,l_n=M_n):Record(l_1:A_1,…,l_n:A_n)}\\ \\ &\frac {\begin{gather} (Val\ Record\ Select) \\ \Gamma \vdash M:Record(l_1:A_1,…,l_n:A_n)\ \ \ \ j \in 1..n \end{gather}} {\Gamma \vdash M.l_j:A_j} \\ \\ &\frac {\begin{gather} (Val\ Record\ With) \\ \Gamma \vdash M:Record(l_1:A_1,…,l_n…A_n)\ \ \ \ \Gamma,x_1:A_1,…,x_n:A_n \vdash N:B \end{gather}} {\Gamma \vdash (with (l_1=x_1:A_1,…,l_n=x_n:A_n) := M\ do\ N):B} \end{align}\]

Variant Types

与 recotd types 和 product 的关系类似，variant types 也由 union types 迭代而来。Union types \(A_1 + A_2\)在 variant types 中可以被定义为\(Variant(left:A_1, right:A_2)\)。

\[\begin{align} &\frac {\begin{gather} (Type\ Variant)\ \ \ \ (l_i distinct) \\ \Gamma \vdash A_1 … \Gamma \vdash A_n \end{gather}} {\Gamma \vdash Variant(l_1:A_1, …, l_n:A_n)} \ \ \ \ \frac {\begin{gather} (Val\ Variant)\ \ \ \ (l_i distinct) \\ \Gamma \vdash A_1 … \Gamma \vdash A_n \ \ \ \ \Gamma \vdash M_j:A_j \ \ \ \ j \in 1..n \end{gather}} {\Gamma \vdash variant_{l_1:A_1,…,l_n:A_n}(l_j=M_j):Variant(l_1:A_1,…,l_n:A_n)}\\ \\ &\frac {\begin{gather} (Val\ Variant\ Is) \\ \Gamma \vdash M:Variant(l_1:A_1,…,l_n:A_n)\ \ \ \ j \in 1..n \end{gather}} {\Gamma \vdash M\ is\ l_j:Bool} \\ \\ &\frac {\begin{gather} (Val\ Variant\ As) \\ \Gamma \vdash M:Variant(l_1:A_1,…,l_n…A_n)\ \ \ \ j \in 1..n \end{gather}} {\Gamma \vdash M\ as\ l_j:A_j} \\ \\ &\frac {\begin{gather} (Val\ Variant\ Case) \\ \Gamma \vdash M:Variant(l_1:A_1,…,l_n…A_n)\ \ \ \ \Gamma, x_1:A_1 \vdash N_1:B … \Gamma,x_n:A_n \vdash N_n:B \end{gather}} {\Gamma \vdash (case_B\ M\ of\ l_1=x_1:A_1\ then\ N_1\ |…|\ l_n=x_n:A_n\ then\ N_n):B} \end{align}\]

Reference Types

引用类型在命令式语言中很常见，它用来包裹地址可变的元素。可以由 ref 分配，由 assign 更新，并由 deref 解除。

\[\begin{align} &\frac {\begin{gather} (Type\ Ref) \\ \Gamma \vdash A \end{gather} }{\Gamma \vdash Ref\ A} \ \ \ \ \frac {\begin{gather} (Val\ Ref) \\ \Gamma \vdash M:A \end{gather} } {\Gamma \vdash ref\ M:Ref\ A} \\ \\ &\frac {\begin{gather} (Val\ Deref) \\ \Gamma \vdash M:Ref\ A \end{gather} } {\Gamma \vdash deref\ M:A} \ \ \ \ \frac {\begin{gather} (Val\ Assign) \\ \Gamma \vdash M:Ref\ A \ \ \ \ \Gamma \vdash N:A \end{gather} } {\Gamma \vdash M:=N:Unit} \end{align}\]

Recursive Types

递归类型需要为环境中扩展一个类型变量 X。类型变量的应用形式为\(\mu X.A\)。例如有一个树类型\(\alpha = unit + int \times \alpha \times \alpha\)，我们可以将等式写为\(\alpha = \tau\)，如果存在\(\tau\)不是\(\alpha\)，且有唯一解使等式成立的情况。那么我们将这个解写为\(\mu \alpha . \tau\)。我们通过方式表示这个 recursive type。由于在这里\(\alpha = \tau\)，那么等式\(\mu \alpha . \tau = \tau \{\frac {\mu \alpha . \tau} {\alpha}\}\)是成立的。我们把从做向右变换的操作称为 unfold ，把从右向左变换的过程称为 fold 。

\[\begin{align} &\frac {\begin{gather} (Env\ X) \\ \Gamma \vdash \diamond \ \ \ \ X \notin dom(\Gamma) \end{gather} }{\Gamma, X \vdash \diamond} \ \ \ \ \frac {\begin{gather} (Type\ Rec) \\ \Gamma, X \vdash A \end{gather} } {\Gamma \vdash \mu X.A} \\ \\ &\frac {\begin{gather} (Val\ Fold) \\ \Gamma \vdash M:[\mu X.A/X]A \end{gather} } {\Gamma \vdash fold_{\mu X.A} M:\mu X.A} \ \ \ \ \frac {\begin{gather} (Val\ Unfold) \\ \Gamma \vdash M:\mu X.A \end{gather} } {\Gamma \vdash unfold_{\mu X.A} M:[\mu X.A / X] A} \end{align}\]

Type Parameters

我们使用一种新语法来表示类型的参数：\(\lambda X.M\)，表示程序 M 中有类型变量 X，例如对于 id 函数\(\lambda x:A.x\)就可以被写为带有类型变量的：\(id \triangleq \lambda X.\lambda x:X.x\)，将类型 A 代入 X，写为 id A ，就可以得到\(\lambda x:A.x\)。

Universally Quantified Types

对应新的项：\(\lambda X.M\)，我们有新的universally quantified types，前式可写为\(\forall X.A\)，表示对于所有的 X，程序体 M 都有类型 A。例如上文中的 id 为：\(\forall X.X \rightarrow X\)，表示对于所有的 X， id X 都有类型 \(X \rightarrow X\)。

基础构成

语法

System \(F_2\)的类型如下，由于我们有了类型参数，所以 System \(F_1\)中的基础类型 K 被去掉了。

\[\begin{align} A, B &::=\ types \\ &X &type\ variable \\ &A \rightarrow B &function\ type \\ &\forall X.A &universally\ quantified\ type \\ M,N &::=\ terms \\ &x &variable \\ &\lambda x:A.M &function \\ &M N &application \\ &\lambda X.M &polymorphic\ abstraction \\ &M A &type\ instantiation \end{align}\]

断言

对于\(F_2\)，断言和\(F_1\)完全相同：

\[\begin{align} &\Gamma \vdash \diamond\\ &\Gamma \vdash A \\ &\Gamma \vdash M:A \end{align}\]

规则

相比\(F_1\)，\(F_2\)的类型环境添加了类型变量 X。

\[\begin{align} &\frac{\begin{gather} (Env\ \varnothing)\\ \ \end{gather} }{\varnothing \vdash \diamond} \ \ \ \ \frac{\begin{gather} (Env\ x)\\ \Gamma \vdash A\ \ \ \ x \notin dom(\Gamma) \end{gather} }{\Gamma,\ x:A \vdash \diamond}\ \ \ \ \frac {\begin{gather} (Env\ x)\\ \Gamma \vdash \diamond \ \ \ \ X \notin dom(\Gamma) \end{gather}} {\Gamma , X \vdash \diamond} \\ \\ &\frac{\begin{gather} (Type\ X)\\ \Gamma', X, \Gamma'' \vdash \diamond \end{gather} }{\Gamma', X, \Gamma'' \vdash X}\ \ \ \ \frac{\begin{gather} (Type\ Arrow)\\ \Gamma \vdash A\ \ \ \ \Gamma \vdash B \end{gather} }{\Gamma \vdash A \rightarrow B} \ \ \ \ \frac{\begin{gather} (Type\ Forall)\\ \Gamma X, \vdash A \end{gather} }{\Gamma \vdash \forall X.A} \\ \\ &\frac{\begin{gather} (Val\ x)\\ \Gamma',\ x:A,\ \Gamma'' \vdash \diamond \end{gather} }{\Gamma',\ x:A,\ \Gamma'' \vdash x:A}\ \ \ \ \frac{\begin{gather} (Val\ Fun)\\ \Gamma,\ x:A \vdash M:B \end{gather} }{\Gamma \vdash \lambda x:A.M:A \rightarrow B}\ \ \ \ \frac{\begin{gather} (Val\ Appl)\\ \Gamma \vdash M:A \rightarrow B\ \ \ \ \Gamma \vdash N:A \end{gather} }{\Gamma \vdash M N:B} \\ \\ &\frac{\begin{gather} (Val\ Fun2)\\ \Gamma, X \vdash M:A \end{gather} }{\Gamma \vdash \lambda X.M:\forall X.A}\ \ \ \ \frac{\begin{gather} (Val\ Appl2)\\ \Gamma \vdash M:\forall X.A \ \ \ \ \Gamma \vdash B \end{gather} }{\Gamma \vdash M\ B : [B/X]A} \end{align}\]

Appl2 中的 \([B/X]A\) 是指用 B 替换 A 中出现的 X。

Existentially Quantified Types

与 universally quantified types 相反，existentially quantified types 表示存在某个类型可以满足等式。

\[\frac {\begin{gather} (Type\ Exists) \\ \Gamma, X \vdash A \end{gather} }{\Gamma \vdash \exists X.A} \ \ \ \ \frac {\begin{gather} (Val\ Pack) \\ \Gamma \vdash [B/X]M:[B/X]A \end{gather} } {\Gamma \vdash (pack_{\exists X.A}X = B\ with\ M): \exists X.A} \\ \\ \frac {\begin{gather} (Val\ Open) \\ \Gamma \vdash M:\exists X.A \ \ \ \ \Gamma,X,x:A \vdash N:B \ \ \ \ \Gamma \vdash B \end{gather} } {\Gamma \vdash (open_B\ M\ as\ X, x:A\ in\ N):B}\]

关于 pack 和 open， 这篇文章 的解释非常详细，推荐阅读。

子类型的定义很简单：如果 A 是 B 的子类型，则任何 A 中的元素都属于 B，记为：$ A <: B$。带有子类型的系统的断言如下：

\[\begin{align} &\Gamma \vdash \diamond\\ &\Gamma \vdash A \\ &\Gamma \vdash A <: B \\ &\Gamma \vdash M:A \end{align}\]

Contravariant & Covariant

逆变(contravariant)和协变(covariant)是与子类型密切相关。如果有函数类型\(A \rightarrow B\)和\(A' \rightarrow B'\)，前者是后者的子类型。那么 A 一定接受任何 A'，所以 A'是 A 的子类型，而产生的 B 一定属于任何 B'，那么 B 是 B'的子类型。可以看出参数的子类型方向变化和函数整体是相反的，所以 A 是逆变的。而返回结果则是一致的，所以 B 是协变的。

总是出现在第奇数个箭头左边的类型是函数类型的逆变。

子类型可以于\(F_1\)和\(F_2\)结合，没有难以理解的部分，推荐阅读原文 。