关于Bot类型一直有所疑惑,是因为相关概念之间没有建立联系。
于是,来回翻书整理如下:
Bot类型中没有一个闭值——P128
我们没有将error包含在值的语法中,只是在项的语法中——P113
每个值都是一个范式,不是值的范式在运行时间错误分析中起着极其重要的作用——P23
项的子集称为值,表示求值的最终结果——P21
如果没有求值规则可以作用于项t,则该项是范式——P23
如果一个封闭项是一个范式但不是一个值,则称该项受阻——P26
一个不含自由变量的项称为封闭项——P34
我们允许在任何上下文中提升一个异常,项error的形式可以有任何的类型。
error类型的这个灵活性在实现类型检查算法时会提高难度,因为它破坏了下面的性质:每个在语言中可类型化的项有唯一的类型。
这能用几种方法来处理,在带有子类型的语言中,我们能给error赋予最小类型Bot,它在必要时可以提升为任何其他类型
在带参数多态的语言中,能给error多态类型forall X.X,它能实例化为任何其他类型。——P113
总结:
项:t ::= error:Bot
(error是一个合法的项,且具有类型Bot
值:v ::= 空
(Bot类型没有值
类型:T ::= Bot
(定义Bot是一个类型
求值规则:空
(没有对应于项error的求值规则,error是范式,但不是一个值
类型规则:Bot<:T
(定义Bot类型是任意其他类型的子类型