Type System and Programming Languages

Table of Contents

类型系统简述

类型系统的性质

  • decidably verifiable: 存在一个检查类型的算法保证程序行为正常。
  • transparent: 程序员应该能够容易判断程序是否可以通过类型检查,如果失败,原因也应该是显然的。
  • enforeable: 尽可能静态地检查类型声明,否则动态检查。

类型系统的形式化定义

类型系统是程序行为的静态近似,帮助我们保证程序的安全性,进行编译阶段的垃圾回收,在运行时之前找到错误。

  1. syntax
    • 分为 type 和 terms,前者描述程序的静态信息,后者(statement, expression, etc.)表达程序的算法行为。
  2. scoping rule
    • 绑定 identifier 和声明的规则。
    • lexical scoping: 静态绑定。
    • dynamic scoping: 运行时才能确定的绑定(例如 RTTI)。
    • 通过制定程序中自由变量的绑定关系,我们确定了一个 scoping。
  3. type rules
    • \(M:A\) 表示 terms \(M\) 具有类型 \(A\) 。
    • \(A<:B\) A 是 B 的子类型。
    • \(A=B\) A 与 B 属于同一类型。
    • \(\Gamma \vdash M:A\) 在环境 \(\Gamma\) 中 \(M\) 有类型 \(A\) 。
  4. semantics

类型的等价性: structural equivalence/by-name equivalence

类型系统的语言

断言

\[ \Gamma \vdash \Im \]

表明 \(\Gamma\) 蕴含 \(\Im\) ,其中 \(\Im\) 中的自由变量在 \(\Gamma\) 这个环境(一个储存变量及其类型的无序表,形式为 \(\emptyset,x_1\vdash A_1\cdots x_n\vdash A_n\) , \(\emptyset\) 为空环境)中有声明。

\(\Gamma\) 中的变量用 \(dom(\Gamma)\) 表示。

最重要的断言是类型断言,例如

\[ \Gamma \vdash M : A \]

表示 \(M\) 在 \(\Gamma\) 中有类型 \(A\) 。

其它的例子

\[ \emptyset \vdash true : Bool \] \[ \emptyset, x: Nat \vdash x+1 : Nat \]

特别的, \(\Gamma \vdash \diamond\) 表明 \(\Gamma\) 是 well-formed 的。

断言有 valid 和 invalid 之分,所有断言均 valid 表明一个程序是 well-typed 的。

类型规则

type-rules.png

例子

type-rules-example.png

类型推导 (type derivation)

给定类型系统的推导是一颗由断言组成的倒过来的树结构,每个断言都由其孩子节点(上方)推导得出。

type-derivations.png

良类型和类型推断(type inference)

当存在一个 type \(A\) 使得 \(\Gamma \vdash M:A\) 是 valid 的,则我们称 term \(M\) 在环境 \(\Gamma\) 下是良类型的。

类型推理是探索一个 term 的推导(及类型)的过程。

在多态存在的情况下,类型推断会变得困难。

类型可靠性(type soundness)

一个类型系统是类型规则的集合,良定义与程序的正常行为的语义相对应。

对于操作语义我们希望

  • 如果 \(\emptyset \vdash M : A\) 且 \(M\) 可以规约到 \(M'\) ,那么 \(\emptyset \vdash M' : A\) 。

对于指称语义我们则希望

  • 如果 \(\emptyset \vdash M : A\) ,那么 \([\![ M ]\!] \in [\![ A ]\!]\) , 表示 \(M\) 的值属于类型 \(A\) 指称的值集合。

TODO 一阶类型系统

无类型 lambda 表达式

f1-syntax.png

f1-judge.png

f1-rules.png

f1-deri.png

TODO 命令式语言的一阶类型系统

TODO 二阶类型系统

TODO 子类型

TODO 等价性

TODO 类型推断

TAPL(Types and Programming Languages)

语义(Semantics)

Semantic 指定了求值规则。

Operational Semantics

操作语义定义一个 abstract machine 来制定语言的行为,抽象机接收语言中的 term 作为机器码,根据内容进行状态转移。

如下定义的是布尔类型的语法和语义:

boolean.png

其中 \(t\longrightarrow t'\) 表示 \(t\) 由一步求值到 \(t'\) 。

有两种定义操作语义的风格: small-step/big-step。

  • small-step 指定单步如何重写一个项,直到它变成一个具体的值 (又称为 reduction)。
  • big-step 直接定义一个项如何求值成最终的值。

算数类型的小步语义定义如下

small-step.png

算数类型的大步语义

big-step.png

其中 \(t \Downarrow v\) 表示 \(t\) 最终求值为 \(v\) 。

Denotational Semantics

在指称语义下,一个项 t 的含义为一个数学对象。

定义一个语言的指称语义需要找到一个 semantic domain 的集合,以及一个解释函数将 term 映射到这些 domain 的元素中。

Axiomatic Semantics

公理语义通过每条语句的 precondition->postcondition 的规则本身定义程序行为。

TODO PFPL(Practical Foundations of Programming Languages)

Author: expye(Zihao Ye)

Email: expye@outlook.com

Date: 2020-06-30

Last modified: 2021-02-19 Fri 21:14

Licensed under CC BY-NC 4.0