类型系统

在一门语言设计中，类型系统是绕不开的。为此分成了两派，动态类型和静态类型。动态类型的语言比如像javascript，lua，python，lisp这类，静态类型比如C，C艹，java这些。至于好坏，各有升秋吧，动态一些的灵活，表达力强，但更容易出现runtime错误，重构的时候也是相当痛苦的。静态类型的更加安全性一些。

这里根强类型弱类型区分一下，概念上的东西。一旦变量的类型确定下来，之后不可以给它赋予其它类型的值，这样的语言是静态类型。反之，像a = 3; a = true这样就是动态的了，变量a先是int类型，能够再给它赋值布尔类型。

强类型是变量上就有类型的概念，而弱类型对于变量是没有类型概念的，只有值才有类型。比如C里面int a =3，变量a是绑定了类型的，而lua里面a = 3并没有给a绑定类型，只有3这个值才绑定了类型。

曾经有次凌晨2、3点写一段OCaml的代码，由于太困大脑已经不清醒了，反正那种状态写的代码我是没信心它能跑的。结果呢，编译通过后，运行直接就OK！这就是OCaml，类型安全的语言。换作其它语言，我敢肯定不出意料会panic，更别提能跑起来没bug。所以，有类型检查还是非常重要的，可以在编译时期就避免掉许多的问题。我需要静态类型，强类型！

带类型的语言一种做法是类型声明，所有变量都把类型写出来，比如C语言。问题是，丑，麻烦。另一种做法是，自动类型推导。像OCaml这类，不需要手动把类型写下来，由编译器自动推导变量的类型。

类型推导是有它的问题。最常见的是一种叫做HM类型推导的算法。最基本的HM类型推导会遇到这种情况：

let id x = x in (id true, id 0)

在id true的时候基础的HM算法会推导出id的类型是bool->bool，然而后面再给id传一个int类型，就会出错了。这个case用术语说，叫做let-polymorphism。针对let-polymorphism，也有补救办法解决，但只能算是一些workround。

再举个例子

let f x = (f 3), (f true)

这个放在动态语言中是OK的，比如x是id函数，'t->'t就应该合法。但是呢，基于HM的系统是推导不出来的。为什么？本质上这个系统在推导时假设类型是一阶的，而实际上这个例子超越了一阶的场景。

总而言之，HM的类型推导是很有局限性的。为此，有更牛(复)逼(杂)的系统被设计出来，比如System F以及更复杂的。但是给我的感觉是，水太深，而且解决一个问题时，总在引出更多的问题。研究下去容易走到两个极端：一个是很复杂，并根本不能实用的系统，纯学术。另一个是发现这个研究方向有些是根本无法解决的问题，然后彻底放弃类型推导。

也不应该因噎废食，类型推导有它的价值。结合一些简单的推导，类型标注才是正确的方向。如果一门语言需要使用者理解背后的知识，绝对不靠谱。我需要类型系统足够简单，推导算法也是足够简单。

十一的那几天，乘着放假，把TAPL(Types And Programming Language)大略的扫了一下。里面有讲从无类型lambda演算，到typed lambda calculus，然后是基本类型扩展，到子类型、递归类型。

基本的像int bool这类没什么好说，然后是函数类型，接下来tuple、record、variant。一个一个讲，先看函数。let id x = x只能推导出't->'t，没有使用时是不能推导到具体类型的。然而id被使用的位置(作用域)是不确定的，在一个地方调id 0，另一个地方调id true。是不是跟什么有一点什么似曾相识？变量的动态作用域！！！

动态作用域是很evil的，这是定论了，所有现代语言都采用静态作用域。把这个类比放到类型推导上面，类型推导其实是使用在动态作用域的，我觉得这才是很多问题的根源。然而也正是这个evil的特性，才能够有抽象类型，静态类型才获得了动态类型的表达能力。

tuple类型是record类型的简化，带名字是record，不带field名字的是tuple。

v = (true, 3, "test")
v = {a=true, b=e, c="test"}

record在其它语言，比如C或者Go，是结构体的概念。里面有一些field，每个field都是自己的类型。相当于类型的"和"。

variant是类型的"或"的语义，选择多个类型其中一种：

type option = Some of int | None

在ML系或者Haskell比较常见，有一点类型于C语言的union。None其实是等价于None of unit

引用variant或者record之后，会遇到的问题：参数化类型 – 泛型。可以把类型看作一个容器，它里面有其它抽象类型，比如

type 'a option = Some of 'a | None

或者换成其它语言的写法

type option union {
    Some T
    None unit
}

关于一门语言设计时是否应该支持泛型，我也是想了又想。否决掉，又加进来，再否决掉...加入泛型后，仅语法层面就要复杂一个级别。更别说语义。如果说表达式是一个维度，那么类型又是一个维度，而泛型再会再加一个维度。不是简单的加一个feature，每加一个维度，复杂度都会乘一个N，大脑立马暴掉了。泛型带来的好处，是否值得它引入的复杂度？往反面讲，需要用于泛型的地方，无非是容器类(比如hash表)，算法类(比较排序)，其它使用场景很小。至于算法类，对函数式语言并不需要泛型就能实现，那么只有容器类需要用到。

但是呢，往正面讲，没有泛型根本玩不出花样来。连list都写不了。一个是[1, 2, 3]一个是[true, true, false]同样都是list，但是没有泛型怎么写？至于monad直接废掉了，bind :: aM -> aM2b -> bM，根本就没有参数化的a。

先假设variant和record都不支持泛型，必须具体类型。但仅仅是引入variant和record以后，就会遇到子类型和递归类型的问题。子类型是，假设A和B都具有相同子类型，那么推导的时候要考虑进去，选择最小的类型子集。后果是使用类型检查和类型推导变复杂。递归类型就更复杂了，类型里面还可以引用到其它类型，比如

type tree = Leaf | Node of tree * tree

如果在类型系统中加入variant、record这些元素以后，事情会变得越来越复杂。所以能不能找到方法即不引入复杂度，又能提供足够的功能。答案是做减法，能去掉都去掉。

加入variant时，我发现在实现时会将variant的值定义为tag+具体值，根据tag来选择。假设我们只匹配类型，看下面：

match x with 
| Some 5 -> xxx
| None -> yyy

编译转换一下其实是：

switch get_tag x {
    case 0: xxx  // 在内部都没有名字概念了，Some用tag为0表示，用tag为1表示None
    case 1: yyy
}

这个过程说明，variant是可以用record实现出来的，由tag + value做"和"的语义，使用的时候判断tag知道是选择variant的哪一种子类型。也就是说，可以不需要variant。

出现类型递归定义的原因是我们引入了"名字"，为某个类型命了一个名，在record里面再用名字指代时，就可能出现递归。想想是不是？不给类型定义名字就没有办法引用，就不会有递归。那么record去掉名字后是什么？tuple！只有tuple行不行？

record无非是tuple加个名字，如果没有名字，照样能干活，field是一个函数，用于取tuple中第i项：

field 2 (21, bool, "abc")
{a=21, b=bool, c="abc"}.c

完全是等价的。只是每次写函数麻烦一些。这个麻烦是值得的，大大简化了语言的设计。下面的代码一样可以工作：

let option tag value = (tag, value)
let Some v = (0, v)
let None () = (1)
switch field 0 (tag, value) {
    case 0:
    case 1:
}

没有泛型，甚至没有record和variant...只是相当于在无类型lambda上加了一个类型推导，这个类型推导非常容易做。没有引入复杂性。关键点就是不为类型引入名字。所有类型的实例都由函数生成。

总结一下，本文在思考如何设计一个合理的类型系统？思路是这样子的：

• 有类型和无类型，选择有类型，因为安全；
• 类型推导会遇到问题，水很深；
• 控制复杂度，标注和推导，选择简单推导；
• 泛型是否必要，复杂度；
• 扩展tuple、variant、record过程中会引入的复杂性；
• 如何做减法，去掉feature，保留等价能力；