第0节 - 不同的类型系统

Makabaka18802025年6月17日...大约 2 分钟

第0节 - 不同的类型系统

编程语言这么多，它们都说自己有“类型”。有人说 Python 是弱类型，有人说 Java 是强类型，也有人在聊什么“System F”……那我们不妨从头捋一捋：到底什么是“类型”？类型系统到底是“系统”在哪？

那到底，什么是类型（Type）呢？

第一次在计算机课上打开Dev C++，老师告诉你类型就是程序中数据的标签或分类，它告诉我们“这个数据是什么样的”、“能对它做什么操作”。

一个数字 42 的类型是“数字” (Int)
一段文字 "Hello" 的类型是“字符串” (String或者Array<Char>)
一个函数 f 的类型可能是“从数字到数字”的函数。(int -> int 或者 $\Gamma \vdash \text{int} \to \text{int}$ )

通过给数据贴上类型标签，程序员和编译器都能更好地理解代码的结构和含义。

等到你学到再高等的算法结构之后，你发现计算机中处处是数学。从数学角度来说，类型是一个集合。有一些运算只能是特定集合内的元素才能进行，就像是群一样，而对于这些集合的运算，我们可以得到各种各样神奇的类型。两个集合的并集对应和类型（Sum Type），笛卡尔积对应积类型（Product Type），函数类型可以看作集合之间的映射，而类型之间的子集关系也能刻画出“子类型”的概念。从这个角度看，类型系统就像是一门关于集合与映射的代数。

事实上，类型在数学中目前最常见的是笛卡尔闭合范畴 (Cartesian Closed Category, CCC)。这是一种更加抽象的数学模型，但可以为安全性分析带来很多有利的工具。

准备好了的话，就进入第一章吧！

下一页 - 弱类型与强类型系统

你认为这篇文章怎么样？