From 8b4c31f9ecef5ce671e227503d6c838df8266751 Mon Sep 17 00:00:00 2001 From: chuigda Date: Mon, 20 Nov 2023 18:06:18 +0800 Subject: [PATCH] =?UTF-8?q?=E6=96=BD=E5=B7=A5?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- markdown/basic-polymorphic-typechecking.md | 48 ++++++++++++++++++++++ 1 file changed, 48 insertions(+) diff --git a/markdown/basic-polymorphic-typechecking.md b/markdown/basic-polymorphic-typechecking.md index 170a11e..39876bd 100644 --- a/markdown/basic-polymorphic-typechecking.md +++ b/markdown/basic-polymorphic-typechecking.md @@ -17,4 +17,52 @@ ## 1. 介绍 +多态类型检查（Polymorphic typechecking）的基础是 Hindley 所设计的类型系统 [Hindley 69]，并在之后被 Milner 再次发现并进行了扩展 [Milner 78]。这个算法在 ML 语言 [Gordon 79, Milner 84] 中被实现。这种类型系统具有和 Algol 68 一样的编译期检查、强类型和高阶函数，但因为它允许多态 —— 也就是定义在多种类型的参数上具有统一行为的函数，所以它更加灵活。 + +Milner 的多态类型检查算法是非常成功的：它健全、高效、功能丰富且灵活。它也可以被用于在没有类型信息（untyped）或者只有部分类型信息（partially typed）的程序中推导出类型。 + +然而，多态类型检查只在一小部分人群中得到了使用。目前的出版物中只有 [Milner 78] 中存在对这个算法的描述，并且其行文相对专业，更多地面向理论背景。 + +为了让这个算法能够为更多的人所接受，我们现在提供了一个 ML 实现，这个实现非常类似于 LCF，Hope 和 ML [Gordon 79, Burstall 80, Milner 84] 中所使用的实现。尽管有时候人们会为了逻辑清晰而牺牲性能，但这个实现还是相对高效的，并且可以被实际地用于大型程序的类型检查。 + +本文中的 ML 实现只考虑了类型检查中最基本的情况，并且许多对常见编程语言结构的扩展都相当明显。目前已知的非平凡扩展（本文不会讨论）包括重载、抽象数据类型、异常处理、可更新的数据、带标签的 record（labelled record）以及 union 类型。许多其他的扩展仍然处于研究之中，并且人们普遍认为在类型检查的理论与实践中，重要的发现尚未浮出水面。 + +## 2. 一个简单的应用序（Applicative）语言 + +本文所使用的语言是一个简单的带有常量的类型化 lambda 演算（typed lambda calculus），这被认为是 ML 语言的核心。求值机制（call-by-name 或者 call-by-value）并不影响类型检查。 + +下面给出表达式的具体语法；相应的抽象语法在本文结尾处由程序中的 `Term` 类型给出（不含解析器与打印）。 + +``` +Term ::= Identifier + | 'if' Term 'then' Term 'else' Term + | 'fun' Identifier '.' Term + | Term Term + | 'let' Declaration 'in' Term + | '(' Term ')' + +Declaration ::= Identifier '=' Term + | Declaration 'and' Declaration + | 'rec' Declaration + | '(' Declaration ')' +``` + +只要在初始环境中包含一系列预定义的标识符，就可以想这个语言中引入新的数据类型。这样在扩展语言时就不需要修改语法以及类型检查算法。 + +例如，以下程序定义了一个阶乘函数，并且对 `0` 应用它 + +```ml +let rec factorial n = + if zero n + then succ 0 + else (times (pair n (factorial (pred n)))) +in factorial 0 +``` + +## 3. 类型 + +一个类型可以是一个用于表示任意类型的类型变量（type variable），如 α、β，也可以是一个类型运算符（type operator）。`int`（整数类型）和 `bool`（布尔类型）是无参（nullary）类型运算符。而 `→`（函数类型）和 `×`（积类型）这样的参数化（parametric）类型运算符则接受一个活多个类型作为参数。以上运算符最为一般化的形式是 `α → β`（任意函数的类型）和 `α × β`（任意序对的类型）。包含类型变量的类型被称为*多态（polymorphic）的*，而不含类型变量的类型被称为*单态（monomorphic）的*。常规的编程语言，例如 Pascal 和 Algol 68 等，其中的类型都是单态的。 + + + > 施工中，请等待施工完成 \ No newline at end of file