[关闭]
@darwin-yuan 2016-07-03T02:49:33.000000Z 字数 10182 阅读 2777

Hindley-Milner类型系统(3)

类型系统 Haskell


我们已经了解了HM类型系统的六条规则,但我们如何可以用它做什么?

答案是:类型推导类型检查

类型推导的职责是:在一个类型系统设定的环境里,给出任意一个符合语法的表达式,类型推导器可以自动推断出其唯一最为通用的类型,它被称做Principal Type

如果一个表达式的Princple Type不存在,或者不可确定,则推导失败。而在类型推导的过程中,会伴随着类型检查。如果发现不符合类型系统规则的情况,也会导致失败。下面就是这个目标的形式化定义:

在一个类型系统下,一个表达式可能具备的最为通用的类型被称为Principal Type。类型推演的目标就是找到任意表达式的Principal Type

为了明白上述规则如何帮助我们完成这个目标,我们再来回顾一下这门简单语言的语法构造:

然后,我们对照那六条类型规则。会发现前四条规则:VAR, APP, ABSLET,它们的conclusion部分和这门语言的语法构造是一一对应的。而从逻辑学的角度,如果一个逻辑的前提,是结论的充要条件,那么我们就把结论当作前提,把前提当作我们要推理的结论,反向构造整个推理过程。

但问题在于:另外两条规则:INSTGEN,在这套规则系统中,和语法没有任何直接的对应关系,也没有明确指出应该在什么地方,以什么样的方式,什么样的顺序使用。也就是说,它们尚不能被直接转化成算法。

为了能让规则直接体现为算法,就有必要制定出更加清晰的,让每条规则都有明确选择时机和选择顺序的类型规则。这样,我们只需要根据表达式的语法结构,就可以自然的选择类型规则。

而这样的规则被称作语法制导syntax-directed)规则。

语法制导规则

按照的定义,我们会发现 依然是一个 ,因而,这意味着:

无论如何,所有的都在前面。正如可以写成一样,也可以写成

如果我们用代表其所有参数的集合,那么就可以被定义为:

现在我们定义如下算法:

我们用如下形式来表示这个算法:

另外,对于,我们可以针对它的每一个参数,都用一个在现有环境中尚不存在的全新类型变量来替换,我们就实例化了一个更为具体的类型。比如:

现在我们定义如下算法:

我们用如下形式来表示这个过程:

HM类型系统里,产生这两条规则的原因只有一个,那就是let binding。因为只有在let binding里才能做到多态。

比如: 里,本身的类型是(参见ABS规则),而的类型为(参见LET规则)。这个赋值的过程,就是运用算法的时机。

然后被存储在本地环境里,以方便于里使用时,可以从环境中找到。

而从环境中查找一个变量,正是规则VAR提供的算法。对于我们这个例子,从环境中查找到后,其类型是,而在具体的表达式里,这个类型必须被实例化。这里正是被应用的时机,也是HM类型系统里,唯一需要应用INST规则的时机。

而这也是HM的四条主规则里,只有LETVAR里的类型用到了的原因。

然后我们重新定义VARLET规则,再加上原来的ABSAPP,就得到了如下四条类型规则:


这就是我们想要的语法制导规则。

基于约束的推演

我们得到了一组语法制导的规则。下面我们通过一个例子来看看如果利用这组规则来推导一个表达式的类型。

我们根据类型规则,可以自底向上明确的重建出整个类型的证明树proof tree):

Screen Shot 2016-07-03 at 10.21.21 AM.png-184.7kB
我们可以看到,在这颗证明树上有很多带有标号的,它们的存在是因为,在构建这颗证明树的过程中,碰到的每个term我们都还不知道其真正的类型。

所以,我们先给这些term一个类型标识,被称作元类型变量Meta Type Variable)。然后我们再分析元类型变量之间的关系,最终推演出类型。

而这些元类型变量之间的关系,就是我们得到的一系列约束。伴随着证明树的重建,每次应用一个规则,就会自动产生一个约束

对于上面这个例子,产生的约束及其过程,如下所示:

Screen Shot 2016-07-03 at 10.23.26 AM.png-150kB
我们将所有的约束罗列在一起,然后来分析约束之间的关系。

首先需要明确:我们的目标是推出

至此,我们成功的推出了结果:

表达式的推演结果是一个monotype,如果将其转化为polytype,则运用得到。但这一步骤,只有当之前的表达式,在一个更大的let表达式里对变量赋值时才会发生,比如:

需要特别强调的是,正如我们之前提到的:inst算法,是通过产生全新的类型变量对polytype进行实例化:这就做到做到了一举两得的作用:

  1. 避免了和环境中已有的自由变量冲突的可能性;
  2. 同一个名字f,每次出现,都会产生一次新的实例化,由于实例化后得到的类型是一个monotype。因而f的两次实例化得到的类型是不同的。而这正是实现多态化的关键。

表达式定义的变量,先被泛化为polytype);随后,变量在表达式里的每次出现,其类型都会被实例化为不同的monotype,这就是let polymorphsim的全部秘密。

Unification

对于一组类型等式构成的集合,首先Unfication是一个对等号两侧的类型进行模式匹配变量替换的过程。

对于mototype,简单的检查等式两侧是否属于相同即可,任何一个等式不成立,都导致Unfication的失败。下面是一组例子:

对于带有变量的等式,通过模式匹配,对变量进行求值。比如下面的例子:

一旦找到一个变量的求值,在整个集合内对这个变量进行替换,从而消除掉这个变量。除了我们的目标变量之外,其它的变量都可以消除。

现在回到我们之前的例子。对于一个这样的表达式,无论从其求值语义,还是LET规则,都有先后顺序。

在类型推演过程中,的目的是用来得出变量的类型,然后通过gen将其泛化,然后用于的类型推演中。

因而,我们先对侧产生的约束进行unify

首先,由于unification所需的是等式,所以,我们需要先把inst规则转化为等式,从而得到如下约束集合及unify过程:

然后调用,可以得到。然后在调用右侧产生的inst,然后开始下面的unify过程:

最终,我们成功的推演出表达式的类型为:

通过这个例子,我们可以总结出类型推演的原理:

类型推演,是根据表达式的语法结构,运用语法制导类型规则,得到一组约束,然后对这组约束进行Unify,从而得到表达式类型的过程。

推演过程中的自由类型变量


现在我们看看表达式的类型推演过程。

首先,根据四条类型规则,我们得到了如下证明树:

Screen Shot 2016-07-03 at 10.39.21 AM.png-232.8kB
最外层是一个表达式,但内部是一个表达式。从上一个例子我们知道表达式的类型推演分成了三个步骤。所以,我们首先推演出的类型为:

然后我们运用gen进行泛化。通过查看我们的证明树,可知,属于环境里的自由变量,因而:

然后回到右侧,在VAR规则里,通过inst进行实例化:

最后产生的全部约束为:

不难发现,之前泛化时的自由类型变量,依然存在于现在的约束里。它之所以能成为的自由变量,是因为它是更外层(如果从证明树的角度看,更底层)表达式的类型变量。

外层表达式类型所包含的类型变量,会成为内层表达式类型的自由类型变量

最后,将这些约束进行Unifiy,推演出来的类型为:

失败的推演

演算理论里,如下等价关系成立:

但在HM类型系统下,其类型推演过程会失败。而失败的原因在于表达式。我们先做按照HM类型规则进行一次推演,看看为何会失败。

首先,我们还是先建立其证明树:
Screen Shot 2016-07-03 at 10.44.34 AM.png-185.6kB
根据证明树,我们得到了如下约束:

然后对约束进行unify:

现在,规则集合里,出现了这样带有递归规则的等式,这明显不符合unify规则。从而推演过程失败。

究其原因,是因为的参数是个monotype,在表达式中的两次出现,都必然是同一种类型,而这样的约束肯定无法支持的语义。

HM类型系统下,一个的参数和结果类型都是monotype,但这与函数自身的类型是否是个polytype没有关系。

添加新批注
在作者公开此批注前,只有你和作者可见。
回复批注