类型系统下的语言分类与类型系统基础

类型系统是一种根据计算值的种类对程序语法进行分类的方式，目的是自动检查是否有可能导致错误的行为。
—Benjamin.C.Pierce，《类型与编程语言》（2002）

每当谈到编程语言时，人们常常会提到“静态类型”和“动态类型”。

类型（Typing）通常是开发者在选择语言时经常考虑的主题。

首先，我们简单讨论一下什么是静态类型和动态类型。

（动态类型与静态类型 Kolja Wilcke https://x.com/01k 的插图）

类型系统的基本概念

类型系统（Typing System）是一组规则，定义了如何管理变量、函数和数据的类型。

类型系统的主要目的如下：

防止错误：防止使用错误类型的数据显示问题。
代码稳定性：使程序行为更具可预测性。
优化可能性：利用类型信息让编译器进行优化。

特别是静态类型（Static Typing）和动态类型（Dynamic Typing）的区别在于类型检查的时间点不同。

静态类型（Static Typing）

在编译时（Compile-Time）检查类型。
变量或函数的类型需要提前声明，编译时可以捕捉类型错误。
代表性语言：C、C++、Java、C#、TypeScript、Kotlin

int age = "32"; // 编译错误发生。不能将字符串赋值给整数型变量

优点是可以提前防止类型错误，提高稳定性。

缺点是编写代码时需要提前声明类型，可能导致开发速度较慢。

动态类型（Dynamic Typing）

在运行时（RunTime）检查类型。
不需要提前声明变量的类型，类型在执行过程中确定。

代表性语言：Python、JavaScript、Ruby、PHP

age = 32 # 整数
age = "Thirty-two" # 字符串（允许）

优点是编码灵活，开发速度快。
缺点是类型错误可能在运行时发生，调试困难。

用一句话总结，静态类型是证明某种错误不存在，而动态类型是从该错误中恢复。

那么，这一切是如何开始的呢？

首先，我们需要了解λ演算（Lambda Calculus）。

.基本数论问题中，有些问题可以通过找到一个有效的函数 f 来解决，这个函数可以根据 n 个正整数来计算。
这里，f(x1, x2, ..., xn) = 2 成立的充分必要条件是某个数论命题为真。
—Alonzo Church，《初等数论中的不可解问题》（1936）

λ演算是编程起点的一篇论文。

在这篇论文中，阿隆佐·邱奇首次正式提出了一个新的形式系统——λ演算。
邱奇利用λ演算将可计算性（Computability）这一直观概念进行了数学上的严格定义。
这与图灵机（Turing Machine）一起成为了定义计算能力的强大且有影响力的形式系统之一。

这篇论文的核心结果是解决了当时数学界的难题——判定问题（Entscheidungsproblem）的不可解性。
这篇论文还包含了函数式编程的基础概念，例如匿名函数（Anonymous Function）、高阶函数（Higher-Order Function）和函数应用（Function Application）。

λ演算虽然复杂，但许多数学家和计算机科学书籍作者的总结如下：

将函数视为最基本的操作。
仅通过变量、抽象和应用三个规则即可表达图灵完备性（Turing-Complete）。

然而，λ演算最初没有类型的概念，是一个可以接受“任何东西”的动态模型。
也就是说，早期的λ演算形式由于没有类型，与动态类型有相似之处，
这篇论文后来成为动态类型（Dynamic Typing）的基础。

*图灵完备性（Turing Completeness）：具有图灵完备性的系统可以解决所有图灵机能解决的计算问题。
**图灵机（Turing Machine）：由艾伦·图灵设计的一种抽象机器，现代计算机也遵循这种结构。

《简单类型理论的公式化》（1940年，Alonzo Church）

四年后，阿隆佐·邱奇提出了一个向λ演算添加“类型（Type）”的系统。

这标志着“类型系统”概念的首次出现，规定了每个变量和函数的输入/输出类型，

这项研究后来成为静态类型（Static Typing）形式的基础。

现在，我们已经看到了静态类型和动态类型的历史起点。

接下来，让我们看看λ演算到底是什么。

无类型λ演算（Untyped-λ-Calculus）

λx. x （恒等函数，identity function）
λx. λy. x + y （将两个值相加的函数）

-> 由于没有类型，可以传递任何值，但无法捕获类型错误！

有类型λ演算（Typed-λ-Calculus）

λx: Int. x + 1 // 接受整数输入并加1的函数
λx: Bool. if x then 1 else 0 // 将布尔值转换为整数

-> 明确声明类型以保证安全性！

眼尖的读者可能已经注意到，λ只是一个“接收输入的东西”。

更具体地说，λ是表示“匿名函数（Anonymous Function）”的符号，

λ表达式只是接收某些输入并执行特定操作后返回结果的函数！

让我们用中学数学来解释：

f(x) = x + 2

将其转换为λ表达式：

λx. x + 2

λx → 接收 x 作为输入。 x + 2 → 然后将输入加 2。

因此，λ可以简单理解为“接收输入的东西”。
就像我们在中学时学过的 x 和 y 一样，理解为插入值的概念。
共同点：
x 和 y 等数学变量也起到接收输入的作用。

λx. x + 2 中的 x 也像变量一样工作。

即，当某个值被提供时，它会被代入并计算函数。
区别：
x 和 y 是简单的变量，而λ还扮演“定义函数”的角色。

λx. x + 2 本身可以作为一个“匿名函数（Anonymous Function）”运行。

Lisp可以在一天内学会。但如果你懂Fortran，那需要三天。-Marvin Minsky

这些概念在高级语言从汇编语言进化的过程中得以实现，

那就是FORTRAN和Lisp。

FORTRAN	1957	静态类型	编译时类型检查	执行速度快
Lisp	1958	动态类型	运行时决定类型	灵活的数据结构

FORTRAN - 静态类型的开端
1957年为科学计算发明的第一种高级语言。

特点

采用静态类型系统
在编译时进行类型检查

Lisp - 动态类型的开端
1958年：约翰·麦卡锡（John McCarthy）开发的函数式编程语言

特点

采用动态类型系统
在运行时进行类型检查

语言的历史无穷无尽，因此简单总结一下，
静态类型在FORTRAN中通过编译时类型检查的方式实现，
动态类型则通过运行时动态决定类型并在执行过程中更改类型的方式实现。

补充一句，FORTRAN引入的类型系统并不是严格的类型系统，
严格的静态类型出现在ALGOL系列中，类型系统本身也经历了几十年的不断发展，

但基本上静态类型和动态类型的大框架一直保持不变。

然后，之后将静态类型和动态类型分开，

再进一步分类，让我们来看看这些分类方法。

（华盛顿大学CSE583）

按类型推断分类

public class TypeInferenceExample1 
{
    public static void main(String[] args) 
    {
        // 显式类型声明 (传统方式)
        int number = 10;  // 声明一个整数类型的变量
        double pi = 3.14;  // 声明一个双精度浮点数类型的变量
        String message = "Hello, Type Inference!";  // 声明一个字符串类型的变量
        
        // 类型推断 (使用 var 关键字)
        var inferredNumber = 20; // 推断为 int 类型
        var inferredPi = 3.14159; // 推断为 double 类型
        var inferredMessage = "Welcome to Java!"; // 推断为 String 类型
        
        // 输出变量的值
        System.out.println("Number: " + number + ", Inferred Number: " + inferredNumber);
        System.out.println("Pi: " + pi + ", Inferred Pi: " + inferredPi);
        System.out.println("Message: " + message + ", Inferred Message: " + inferredMessage);
    }
}

（示例是Java著名的强类型推断关键字var）

类型推断（Type Inference）是指程序员无需显式声明类型，编译器（或解释器）通过上下文（Context）或代码结构分析，自动推断变量、函数、表达式的类型的功能。

《类型与编程语言》一书中，

这部分内容以类型重建（Type Reconstruction）的形式出现，类型推断（Type Inference）一词与其混用，

类型重建（Type Reconstruction）被解释为类型推断（Type Inference）的一种形式。

类型推断（Type Inference）

编译器能够完全推断类型的情况

类型重建（Type Reconstruction）

已知部分类型信息，需要推断其余部分的情况

强类型系统提供了更安全的编程，但牺牲了灵活性。

无论如何，尽管各种语言使用不同的类型系统，但基本上分为

强类型系统和弱类型系统。

强类型系统

类型转换（Implicit casting）受到严格限制。

弱类型系统

类型转换自由，可能会导致意外行为。

为了更深入地理解这一点，让我们解释一下Hindley-Milner类型系统。

按Hindley-Milner系统应用与否分类

（表示Hindley-Milner类型系统的规则）

規則	說明	與 Hindley-Milner 類型系統的關係
[Var] 變數規則	環境(Γ)中存在的變數 x 具有類型 σ。	推斷變數類型的基本規則
[App] 函數應用規則	如果 e0 是 τ → τ' 類型，且 e1 是 τ 類型，那麼 e0 e1 是 τ' 類型。	定義函數應用時如何推斷類型
[Abs] Lambda 抽象規則	如果 Lambda 函數 λx.e 的 x 是 τ 類型，那麼結果是 τ' 類型。	基於 Lambda 演算的函數類型推斷方式
[Let] let 綁定規則	在 let x = e0 in e1 中，x 具有 e0 的類型。	ML 系語言中通過 let 進行類型推斷的方式
[Inst] 實例化規則	如果類型 σ' 是 σ 的實例 (⊑)，那麼 e 可以具有 σ 類型。	與多態性(Polymorphism)類型推斷相關
[Gen] 多態性泛化規則	如果 e 具有類型 σ，並且 α 不是自由變數(free(Γ))，那麼 e 可以具有 ∀α.σ 類型。	解釋 Hindley-Milner 的 Let-Polymorphism

Hindley-Milner系统提供了强大的类型推断功能。

基于约束的类型系统 Constraint-Based Typing）

基于约束的类型系统是一种在类型推断过程中收集约束，然后批量解决这些约束（Constraint）的方法。
即，先收集所有必要的关系（约束条件），然后解决问题以确定最终类型。
在函数应用时不立即匹配类型，而是先收集类型约束（Constraint），稍后统一解决（Unification）。

之后，根据开发者是否在代码中显式声明类型（Explicit），或者由编译器/解释器自动推断（Implicit），
语言被进一步分类。

显式类型系统（Explicit Typing）

开发者需要显式声明类型
代码可读性好，但代码可能变长
编译器能准确预测类型，因此错误较少

隐式类型系统（Implicit Typing）

不需要显式声明类型，编译器自动推断
代码简洁，但可读性可能下降
如果推断出错，调试可能困难

也就是说，显式类型系统保证类型安全性，但代码可能冗长；隐式类型系统代码简洁，但可能出现意外的类型推断问题！

现在，基于此分类，让我们对现代常用语言进行分类。

語言	靜態/動態	強/弱類型	明示/暗示	是否適用 Hindley-Milner	特點
C	靜態	弱	明示	否	類型轉換(Implicit Cast)自由（如 int → double）
C++	靜態	弱	明示	否	與 C 相似，但支持部分類型推斷（例如 auto 關鍵字）
Java	靜態	強	明示	否	支持 var，但並非完整的類型推斷系統
C#	靜態	強	明示/暗示	否	支持 var 和 dynamic 關鍵字，部分支持動態類型
Go	靜態	強	暗示	否	使用 := 運算符進行類型推斷
Rust	靜態	強	暗示	部分適用	使用 let 關鍵字，類型推斷能力強
Swift	靜態	強	暗示	部分適用	類型推斷能力強，支持 let 和 var
Kotlin	靜態	強	暗示	部分適用	提供比 Java 更強大的類型推斷
Haskell	靜態	強	暗示	完全適用	基於 Hindley-Milner 的完整類型推斷
OCaml	靜態	強	暗示	完全適用	與 Haskell 類似的類型系統
TypeScript	靜態	強	明示	否	JavaScript 的靜態類型版本
Python	動態	強	暗示	否	運行時類型檢查，typing 模塊支持部分靜態類型
JavaScript	動態	弱	暗示	否	== 和 === 運算符差異存在，隱式轉換能力強
Ruby	動態	強	暗示	否	類型轉換嚴格（例如 "5" + 5 不可能）
Lisp	動態	強	暗示	否	在動態類型語言中，類型非常靈活