1 简介

    探索意味着有一个目标，
    发现却意味着目光自由，胸怀坦然，没有目标。
    
    --黑塞

当我们在编程世界漫游时，比如声明一个变量并为其赋值，内存会以二进制形式保存此值。我们的计数系统是十进制的，这意味着我们每天知道和使用的数字在二进制中非常不同。而类型系统是一组规则，或多或少是严格的。你不能用某些类型做你想做的一切。

编程语言通常有一整套开箱即用的类型。这些类型称为基元类型。例如：integer，boolean，float，string 等。

如果编程语言的类型迫使我们遵守某些规则，那么编程语言需要一种算法来检查我们是否遵守它们。这称为类型检查，本文尝试从框架和技术方面理解这些内容。

2 语言框架

现代软件工程承认应用范围广泛的形式化方法，

以帮助确保系统在某些特定方面正确运行 隐式或明确地表明其期望的行为。

类型系列的一端是强大的框架，例如 数理逻辑、代数规范语言、模态逻辑和指称语义。不同语言有着不同的语言类型系统。

现代常用的开发语言：

用于应用程序和程序开发 – C、C#、C++、GO、D、Java、Swift 和 Tcl。
用于人工智能开发 – AIML、C、C#、C++、Prolog 和 Python。
用于数据库开发 – DBASE、FoxPro、MySQL、SQL 和 Visual FoxPro。
用于游戏开发 – C、C#、C++、DarkBASIC 和 Java。
对于计算机驱动程序 – Assembly 和 C。
对于 Internet 和 Web – HDML、HTML、Java、JavaScript、Perl、PHP、Python 和 XML。
用于脚本开发 – AutoHotkey、awk、bash、Batch 文件、Perl、Python 和 Tcl。

这些可以用来表达非常普遍的正确性属性，但通常使用起来很麻烦并要求程序员有大量的复杂性。

3 语言技术

在另一端是力量更温和的技术，以至于自动检查器可以内置在编译器、链接器或程序分析器中，

因此即使是不熟悉底层框架的程序员也可以熟练应用理论。

这种轻量级形式方法的一个著名实例是模型检查器，在有限状态机系统中搜索错误的工具，

例如：
    芯片设计
    通信协议

一个经典有限状态机是知名的TCP协议：

另一个非常流行的是运行时监控比如runtime，它是一组允许系统运行的技术的集合。

动态检测其组件之一的行为是否符合到规范。

但迄今为止最流行和最成熟的轻量级形式化方法是类型系统，是未来的中心焦点。

类型系统是一种易于处理的句法方法，

用于证明不存在通过根据种类对短语进行分类来确定程序行为他们计算的值。

4 类型系统关注点

有几点值得关注。

这个定义标识类型系统作为推理程序的工具。

这一措辞反映了面向编程语言中的类型系统。
编程语言的类型系统也分为强类型或弱类型（也称为松散类型）。
但是，对于强类型或弱类型系统的构成，没有明确的定义。

对于强类型类型系统，普遍接受的行为是：

  变量确实有类型，您无法更改它。我们需要预先指定变量的类型（显式或隐式）。
  该语言不会隐式更改任何变量的类型。我们必须显式地进行所有类型转换。
  如果类型不兼容，则不能在任何操作中使用变量作为操作数。

比如在强类型系统中，即使我们将一个数字存储为字符串，我们也不能在加法运算中将其用作操作数。要首先使用它，我们需要将字符串显式转换为数字。弱类型反之亦然。JavaScript 是弱类型语言的一个例子。
这些规定使代码更加冗长。但它也使代码更容易理解，因为没有（或减少了）隐藏的行为。

具有静态类型检查的强类型语言包括 Java、Pascal、Ada、C、GO 和 C#。另一方面，Python 具有动态类型检查和强类型。

更一般地，术语类型系统（或类型理论）指的是逻辑、数学和哲学的研究领域，这是更广泛概念。

类型这种意义上的系统在 1900 年代初期首次正式化，

为了避免出现威胁数学基础的逻辑悖论，例如罗素的理发师悖论 (Russell, 1902)。

在二十世纪，类型已成为逻辑中的标准工具，

尤其是在证明论中（参见 Gandy，1976 年和 Hindley，1997 年），并已渗透到哲学语言和科学。

该领域的主要里程碑包括：

   罗素的原始类型理论（Whitehead 和 Russell，1910）、
   拉姆齐的简单类型理论(1925)
   Church 的简单类型 lambda 演算的基础 (1940)
   Martin Löf 的构造类型理论 (1973, 1984)
   Berardi、Terlouw 和 Baren dregt 的纯类型系统 
   (Berardi, 1988; Terlouw, 1989;巴伦德雷格特，1992）。

5 小结

即使在计算机科学中，也有两个主要的研究分支类型系统，动态和静态的。

而更实用的，面向人工智能的，涉及到编程语言的应用，将是重点。

参考：
Luca Cardelli 类型系统：
http://lucacardelli.name/Papers/TypeSystems.pdf

Go中的类型系统
https://golang.org/ref/spec#Types