浅谈类型论——开场白

现在是信息时代，计算所带来的科技革命彻底改变了我们的生活。一些人，一只手机在手忘记所有；一些人的网瘾堪比毒瘾，戒网戒手机已经成为21世纪初叶的心灵鸡汤，这种景象如果在30年前还是难以想象的。

如果你喜爱电脑，或许你还会喜欢编程。如果你喜欢编程那你一定会有心仪的程序语言；如果你懂编程语言，你或许知道面向对象和函数式编程；如果你恰好懂得函数式编程，有很大的几率你知道lambda演算，monad，但是你知道类型论吗？懂得类型论的人肯定不多，但是所有人都知道“类型”意思。

类型，是一个常用词，分开看，类，物以类聚，人以群分，所以相似的对象、观念、思想我们可以归类；型，相当于一个模子，归纳一系列相似的行为、操作、流程，所以“型”又叫模式。这样看，类型其实是人类认识世界最有效的工具，用类型我们可以将世界上成千上万数也数不清的“东西”归纳成让大脑可以容纳的“类”，而“类”的性质、行为、动作可以归纳成“型”——模式，也就是我们常说的“行为模式”。类和型放在一起，就可以看做是有相同或相似行为模式的类的聚集。

如果你恰好对计算机编程感兴趣，那么类型对你就有了更实在的现实意义。你知道同样是3，它的类型可能是字符也可能是数字。任何一个普通名词都可能是一种类型。从哲学的角度，类型回答了一个本体论的核心问题：什么是存在？一个实体的类型就是它存在的理由。而且客体所具有的类型越多对我们人类来说就越容易认知。如果把“幸福”当做一种类型，能说清楚它的真正意义的大概只有哲学家，而把“有车有房”当做一种类型的话，那么人人都是哲学家。

但是，什么是“类型论”？这里，我们先说它不是什么。它不是人生哲学，不是心灵鸡汤，不是致富法门，更不是命理算术。

类型论是一门精密严谨的科学，它即枯燥又有趣，对它的学习过程，是一种典型的“痛并快乐着”的体验。
类型论在科学花园中的位置，大概处于数学、逻辑、计算和语言学的交界处，可以说它生于逻辑，长于数学，开花于计算机科学，结果于语言学。用不那么修辞式的直白说法就是：类型论是20世纪初为为解决逻辑悖论问题提出的解决方案，但是对类型论的形式化研究一直是在数学领域，类型论研究直接导致了一种计算模型的出现，成为理论计算机科学中一个重要分支。对类型的哲学讨论，虽然可以追溯到古希腊亚里士多德时代，但是近现代哲学、特别是数学哲学对类型论的讨论被认为是从弗雷格开始。而Richard Montague从上世纪70年代开始提出了基于内涵逻辑和类型论的语义学，从此类型论成为语言学中重要的工具。

作为和图灵机并列的计算模型，类型论在计算机刚刚面世的10几年中并未如前者成为理论计算机科学的支配性模型，它大器晚成，直到上世纪60年代之后才逐渐为人所重视，并有所发展。其中最重大的成果就是将逻辑学中的证明论和类型论统一为一种理论。如果说图灵机是在无限长度纸带的读写过程，将计算的模型归结为是自动机，一种机器模型，那么，类型论则把计算模型当做可计算函数，它所研究的就是抽象意义的函数，它抽掉了通常数学意义的函数概念，没有数的概念，它抽掉了函数的处理过程的概念，研究函数的本质，将函数这个概念，上升到一种哲学的高度。对类型论的形式化表述，是一种介于数学和逻辑的语言，称作λ-演算，或者lambda演算，或者全中文：兰姆达演算。

在计算机科学领域，图灵机是一种计算机程序设计的理论基础，它的基本原理就是将计算模拟成在无限长度纸带的读写和存储过程的机器；现代许多计算机程序设计语言就是图灵机模式的一种具体实现；

而类型论是与图灵机并列的另一种计算模型，它将计算模拟成函数和函数的叠加、组合，这样计算问题就可以归结为函数问题。而这个思想最早的起源可以追溯到19世纪的弗雷格。而在当代，这种模型逐渐成为显学，具体的表现形式就是另一种编程范式——函数式编程在上世纪80年代的兴起。
类型论的出现，打破了学科之间的藩篱，让一些表面看上去毫无关联的是东西表露出其实是一件东西的本质。类型论使得函数概念不再是数学和逻辑的专利，它使得函数深入到哲学、语言学等领域。
如果能对类型论有一定的理解，那么也会让我们以一种统一的模式看待数学、逻辑、计算、语言学和哲学。这也是科学的进步本质之一：用更加统一的、更加简单的模式理解这个复杂世界。
本系列小文，将探讨类型论的前世今生，但不会讨论函数式编程，更不会讨论特定的编程语言，因为这方面的资源很多。我们只讨论类型论的演进过程，在历史和现实中的作用，以及它的基本内容。如果你恰好也想了解类型论的理论，那么这将是一次激动人心之旅，因为我们将看到数学、逻辑、哲学、计算和语言学中许多不同的概念如何可以统一在类型论下。

中世纪的经院哲学家托马斯·阿奎那曾经说过：

One should realize...that if we consider these four, namely wine, king, woman, and truth, in themselves they are not comparable because they do not belong to the same genus.
Nevertheless, if they are considered in relation to some effect, they coincide in one aspect, and so can be compared each other. 

（应当认识到，当我们在孤立地(in themselves)谈论这些概念，亦即，红酒、国王、女人和真理时，它们是没有可比性的， 因为并不属于同一类别。但是如果将其放在某种效应的关系上谈论，这些概念将在某个方面重合使得我们可以对其相互比较。）