类型系统

2016-10-13

在一门语言设计中,类型系统是绕不开的。为此分成了两派,动态类型和静态类型。动态类型的语言比如像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<T> 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,保留等价能力;
类型系统HMtype infer