[关闭]
@darwin-yuan 2016-07-03T01:19:06.000000Z 字数 8157 阅读 3303

Hindley-Milner类型系统(2)

类型系统 Haskell


类型规则

在关于类型系统的大量文献里,都采用了一种来自于自然推演Natural Deduction)的符号系统来定义类型系统。HM类型系统的规则定义也不例外。为了能够更好的理解后续的内容,我们先来简单介绍一下这套符号系统。

首先,所有的规则都是基于这样的模式:

在右边的NAME是这条规则的名字,可有可无。在线的上方,描述的是前提premise),前提可以由多个判断Judgement)组成;在线的下面,给出的是结论conclusion),结论只能包含一个判断

因而,这种定义可以理解为:

变量查找

现在我们来看第一个规则:

这条规则的名字叫做VAR,表示这是一条变量规则。其中 代表:的类型为 代表已知的事实,在这里可以理解为全局环境。而符号 的意思是:可以推导出

因而,这条规则的意思是:如果一个类型为 的变量 存在于环境 中;我们则可以从环境 得知 的类型是

注意这个规则里出现的类型都是,这就意味着存在于环境里的变量,即可能是个monotype,也可能是个polytype

函数定义

下面我们来看第二条规则:

ABS代表的意思是Abstraction,即Lambda抽象。这里需要介绍一种新语义:在里,由已知事实 ,加上一个新假设的事实 ,可以推导出 。如果回到环境的角度,则 代表全局环境,而 则代表本地环境,它们合在一起,构成一个新环境,从它可以推导出

所以,第二条规则的意思是:假如允许我们引入一个新的、类型为 的变量 ,从而就可以推导出 的类型为 ,那我们就可以知道:从现有环境 可以推导出 的类型为

函数调用

第三条规则用来描述函数调用Function Application),定义如下:

意思很简单:如果由现有环境可以推出的类型为 的类型为 ,那么我们就能推出:的类型为

规则二和规则三,是对偶关系,分别定义函数函数调用相关的类型规则。与这两条规则有关的类型全是,即monotype。这就意味着,在HM类型系统里,lambda的参数和结果,都只能是monotype

对于形如 的类型,如果我们将其看作一个 函数,就会知道,在一次实例化的过程中,其参数 都只能各自被实例化为一种类型。比如:

而对于 这样类型的函数,我们在一个上下文里对 进行实例化后,得到的类型里 依然还是个多态类型。

这就像演算里的高阶函数一样,这种类型被称为类型系统里的高阶类型higher rank type)。

因而,我们可以在同一个上下文里,对这个高阶类型进行多次不同的实例化。比如如下代码,在对高阶类型支持的类型系统下是可以通过检查和编译的。

  1. g :: forall a b. (forall c. c -> c) -> (a, b) -> (a, b)
  2. g f (x,y) = (f x, f y)

但正如我们之前所提到的,在HM类型系统里,所有的 都必须出现在最前面,这也就意味着不允许存在高阶类型。因而函数 的类型在HM类型系统下非法。

Let Binding

我们重新回到类型规则,来看看第四条:

这条规则被称做Let Binding,其意思是:如果由现有环境可以推论出的类型是;同时,如果引入一个类型同样为的临时变量,则可以由现有环境推论出的类型为一个单态类型;那么,我们就可以推论出:表达式的类型为单态类型

从语义上,这条规则似乎没有什么难以理解的。并且,它貌似可以通过ABSAPP两条规则组合而来。毕竟,在算子理论里,等价于

但是,这条规则正是HM类型系统最为特别的地方:由于定义本身不允许高阶类型,因而如下代码完全无法通过类型系统的检查:

  1. (\x -> x x) (\x -> x)

但是,在不引入高阶类型的前提下,Let Binding却可以让上面等价语义的代码通过类型检查,如下:

  1. let f = \x -> x in f f

在这个表达式里,的类型为,正如LET规则所描述的,这是个所允许的多态类型。在表达式里,的两次出现,其类型都是多态类型,因而可以各自实例化:

因而,在HM类型系统里,尽管let binding定义依然具备等价的替换(substitution)语义,但是在类型的宽容度上,两者已经不再等价。所以,在HM类型系统下,let binding不仅仅是一个的语法糖,它提供了更强大的能力。而这种能力被称做LET绑定时多态let polymorphism)。

的单态与多态

HM类型系统下,所有的的类型都是monotype。因而当看到如下定义时,我们必须清楚:等号右边的表达式的类型是,即没有前面的,因而它是monotype

你一定会质疑:明明类型标注上的写的清清楚楚!

没错,但那不是等号右边表达式的类型,而是等号左边的变量id的类型。在HM类型系统下,将monotype转为polytype的唯一方式就是通过LET绑定时多态,即通过等号进行变量绑定时。haskell的顶层,不过是一个隐形的大let语句。

  1. id :: forall a. a -> a
  2. id = \x -> x

事实上,等号右边的完全没有任何理由属于polytype。因为,对于一个定义,如果不将其绑定到任何变量,那么它将只能使用一次,只有变量才让它具备多次被使用的可能性。只需要使用一次,意味着它只可能有一种类型,并不存在多次实例化的需要。

为了更清晰的理解这一点,我们来假设HM类型系统并不支持LET绑定时多态,这种情况下,我们用下面的表达式,与注释里在支持LET绑定时多态情况下的let表达式等价:

  1. (\x -> x) (\x -> x) -- 等价于:let f = \x -> x in f f

这是因为,我们将同一个定义实现了两次。虽然它们的定义看起来一摸一样,但在类型系统的眼里,它们是两个独立的,因而会各自推演它们的类型。并且也确实各自推演出了不同的类型。

因而,站在的外部来看,的类型没有任何理由属于polytype

但是,站在的内部,当它使用一个函数类型的参数时(当然,参数是一个名字),是否支持其参数绑定时多态,将会产生重大的不同。

比如,如下代码里,参数被实例化为不同的类型。而这只有在允许参数绑定时多态的情况下,那行表达式才能通过类型系统的检查。而一旦支持了参数绑定时多态,那么函数的实现里,虽然传入的是一个(我们之前刚刚讨论过,的类型必然是monotype),但其与函数 的参数 进行绑定的过程中,类型会自动升级为polytype

  1. f :: (forall a. a -> a) -> (Bool, Int)
  2. f = \g -> (g True, g Int)
  3. f' = f (\x -> x)

参数绑定时多态,被称做higher rank type。为了支持这种能力,需要程序员给出类型注解。这就违背了HM类型系统设计的初衷。因为HM类型系统的本意,正是在完全不需要程序员给出类型注解的前提下,可以完全推断出所有表达式的类型。

类型泛化

第五条规则被称做泛化Generalization),定义如下:

自由与边界

为了进一步理解polytype里的类型变量,让我们再次回到的世界。

表达式里,变量一共分为两类:

  1. 自由变量Free Variable
  2. 有界变量Bound Variable

比如,表达式的子表达式里,就是有界变量,因为有个同名参数,因而它被约束在的范围内;而由于没有任何参数可以绑定,被称作自由变量

一个表达式里,只有自由变量可以被替换。比如,当我们试图对表达式执行替换操作,我们得到的结果是,只有自由变量 发生了替换,而有界变量 未受影响。

而在同一个表达式里,同一个名字的变量,即可能是自由的,也可能是有界的。这是因为它们虽然都是同一个名字,但事实上代表着不同的变量。比如:里,第一个是一个自由变量,第二个是参数,第三个则是一个有界变量也都是自由变量

如果我们对这个表达式执行替换操作 ,得到的结果是:

现在回到类型的世界。

既然是类型系统里的,同样的道理,对于这样的类型,是一个有界类型变量,而则属于自由类型变量

如果对整个类型执行替换操作,得到的结果是

而对于表达式都是自由类型变量。如果对整个类型执行替换操作,得到结果是

需要强调的是:从的定义可以看出,在HM类型系统里,如果一个类型属于polytype,其所有的都只能出现在最前面

也就是说,我们只能定义形如这样的polytype,而不可能定义这样的polytype

函数则是用来求所拥有的所有自由类型变量,其结果是一个集合。

比如:;而

环境里,存储的是所有已知的的集合。因而,

代表现有环境中所有的自由类型变量的集合。

它的意思是:如果由现有环境可以推导出表达式的类型为,对于里的任意自由变量,如果不存在于 ,那么它就可以成为 参数。

比如,我们基于现有的环境推导出的类型为,这个类型包含三个自由类型变量: 。其中,如果是环境中已经存在的自由类型变量,但不是,那么上述类型就可以泛化为:

所以,为了更清晰的表述,这条规则可以修正为:

类型实例化

最后一条规则称做实例化Instantiation):

这条规则定义里有一个重要的新符号,它表示左边比右边的类型更通用,更泛化,更多态。当然,也可以反过来说,右边比左边的更特殊,更具体。比如:

在其它文献中,也有使用符号的。它们都和一样,代表左边比右边更通用。比如:

但对我个人而言,符号的开口朝向更加通用的类型,更符合我的直觉。因而,本文均采用符号

理解这个符号之后,这条规则的意思也就呼之欲出:如果从现有环境可以推出表达式的类型为,并且更加通用,那么我们就可以从现有环境推出:表达式的类型可以是更加具体的

或许你已经注意到,最后两条规则:INSTGEN是一对互逆的规则。一个表达式的类型可以通过GEN提升到更加通用;相反,也可以通过INST降格到更加具体。

小结

本文介绍了HM类型系统的六条类型规则。在随后的文章里会讨论基于这六条规则的类型推导

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