2 描述类型系统的语言

类型系统概述

类型表达式

• 基本类型：boolean, char, integer, float, void
• 类名
• 数组类型构造算子：array (num, type)
• 记录类型构造算子：record (name, type)
• 函数类型构造算子：typeS → typeT
• 列表（元组）类型构造算子：typeS × typeT

$$\newcommand{\t}{\textbf} \t{int,int}→\t{int}$$

定型断言

$$x:\t{int}\vdash (x+3):\t{int}$$

断言

断言具有如下形式： $$ \Gamma\vdash\mathcal{S} $$ 其中，$\mathcal{S}$ 的所有自由变量都声明在 静态定型环境 $\Gamma$ 中。

静态定型环境 $\Gamma$

形式是 $n$ 个不同名字的变量 $x_1,...,x_n$ 和他们所属类型 $T_1,...,T_n$ 的有序表 $$ x_1:T_1,...,x_n:T_n $$ 相当于程序的类型声明语句和编译器的符号表

在 $\Gamma$ 中声明的这组变量 $x_1,...,x_n$ 用 $dom(\Gamma)$ 表示

断言的种类

典型的断言形式

$\Gamma\vdash S$，$S$ 是一个命题，且 $S$ 中所有的自由变量都声明在 $\Gamma$ 中

定型环境的断言

$\Gamma\vdash\diamondsuit$，表示 $\Gamma$ 是良性的定型环境

类型表达式的语法断言

$\Gamma\vdash\t{nat}$，表示在 $\Gamma$ 下，$\t{nat}$ 是类型表达式

语法项的定型断言

$\Gamma\vdash M:T$，表示在 $\Gamma$ 下，语法项 $M$ 具有类型 $T$

例子：

• $\varnothing\vdash \t{true}:\t{bool}$

可以类比 “公理”，这个断言的成立并不依赖于任何环境中的自由变量

• $x:\t{nat}\vdash (x+1):\t{nat}$（$\t{nat}$ 是自然数集）

推理规则

类型系统的推理规则

$$\frac{前提}{结论}\quad\frac{\Gamma\vdash M:\t{int},\Gamma\vdash N:\t{int}}{\Gamma\vdash (M+N):\t{int}}$$

$\Gamma$ 是定型环境（即符号表）。

这个推理规则的含义是，如果所有前提有效，则结论也有效

环境规则

例子：$(Env\quad\varnothing)$ $$ \frac{}{\varnothing\vdash\diamondsuit} $$ 表示空环境是良形的环境

前提个数可以为 0，这样的规则叫做公理

语法规则

例子：$(Type\quad\t{bool})$ $$ \frac{\Gamma\vdash\diamondsuit}{\Gamma\vdash\t{bool}} $$ 表示 bool 是类型表达式

定型规则

推理规则的结论是定型断言的话，则称之为定型规则

例子：$(Exp\quad+)$ $$ \frac{\Gamma\vdash M:\t{int},\Gamma\vdash N:\t{int}}{\Gamma\vdash (M+N):\t{int}} $$ 表示在环境 $Γ$ 下，$M+N$ 是 int 类型

本文阅读量