深圳网站建设公司联华,大连市招标网公示,网页界面设计和软件界面设计的区别,怎么早网站上放广告史磊 仓颉语言类型推断技术专家
一、一种看待类型系统的方式
一门编程语言一定得包含类型系统吗#xff1f;
这个问题今天看来可能显而易见#xff0c;一个程序没有类型的话还能算是个完整、正确的程序吗#xff1f;但是其实关于类型系统的作用#xff0c;一直是存在两种…
史磊 仓颉语言类型推断技术专家
一、一种看待类型系统的方式
一门编程语言一定得包含类型系统吗
这个问题今天看来可能显而易见一个程序没有类型的话还能算是个完整、正确的程序吗但是其实关于类型系统的作用一直是存在两种针锋相对的看法的。大家普遍习惯的这种把类型作为程序不可分割的一部分的看待方式叫做“内生”intrinsic的理解方式即一个程序如果没有合法的类型就不能算有意义的程序。而与之相对的也存在一种“外生”extrinsic的理解方式持这种观点的人认为程序即使没有类型也同样有意义类型检查只是额外地证明了这个程序的一些性质与其他的各种程序分析工具应该处于同样的地位。
姑且不论类型检查是否应该作为一个语言之外的的工具这种工程问题顺着“类型检查是为了证明了程序的一些性质”这个思路我们可以得到一些很有趣的认知。
不妨想象一下一个程序如果在没有类型的情况下就执行起来会发生什么问题呢我们有可能给一个函数传入一个整数但是这个函数实际上却是处理字符串用的于是它错误地把这个整数形式地数据当做字符串来处理了最后自然是得不到期望的结果。例如下面的伪代码
func f(s) {s.replace(...)
}
let s f(1)
而在这个过程中加入类型系统的话如果可以静态地验证这个被调用的函数的形参类型是一个字符串而每次调用它时实参类型都也是字符串那么我们就可以保证在任何情况下执行这个程序都不会出现把一个整数类型的参数传递给这个处理字符串的函数这种低级错误。
所以这里我们用比较朴素的方式去理解的话类型系统、尤其是静态类型系统实际上是一种“程序在运行时处理数据的方式永远不会出错”的证明如果类型检查可以通过那么每个数据被传递时它的提供者和接收者对于这块数据的格式、可以被执行的操作等等的理解总是一致的。实际上这个性质已经几乎就是一些比较公认的“类型安全”type safety的定义了。
另外细心的读者可能会注意到既然类型系统是一种程序运行时“永远不会出错”的证明那这个证明完成后在程序运行时我们还需要保留“类型”这个东西吗确实如此除了为了支持动态派遣等一些动态特性外大多数静态类型的信息在类型检查完成后对于程序的正确运行就基本没有用处了理论上是可以被擦除掉的。当然实际的实现中类型信息对编译优化也有帮助所以也有语言会选择在后续的编译阶段一直保留它们。
那么我们再回头去看这篇文章最关心的重点问题类型推断是什么类型标注又是什么既然类型检查是一种正确性的证明那开发者提供的类型标注自然就是手写的部分证明而类型推断则是一种自动化证明的技术。自动化证明的算法越聪明必须手写的部分也就越少能支持的类型特性也就越丰富。实际上在一些研究性的语言中类型系统早已超越简单的“处理数据的方式”的正确性证明还可以包括资源消耗、执行时长、数组长度、值的可空性等等多种方面的正确性证明其中的类型推断用到的技术与更一般的形式化证明也越来越接近了。 二、仓颉的类型推断需要做什么
在仓颉语言中类型推断主要起到两个作用第一是确定每个声明和表达式的类型这既包括可以省略的变量类型、函数返回类型、泛型实参类型等等也包括分支、循环、字面量等并不涉及类型标注的各种表达式的类型。第二是帮助确定每个被使用的名字对应的声明最典型的情况是在调用一个重载的函数时需要确定调用的具体是哪个定义另外有些不同种类的定义如果碰巧名字相同我们也可能需要借助类型信息来确定使用的究竟是哪个。 三、基于合一unification的类型推断
在一些早期的编程语言中类型之间并没有子类关系只有相等或不等。时至今日多数函数式编程语言仍然继承了这个设计思路包括 Rust 语言如果不考虑生命周期的话类型之间也没有子类关系。在这些语言中类型推断普遍是基于合一unification过程来完成的。简单来说即是每当我们遇到一个暂不确定的类型那就为它引入一个待解的变元然后在遍历程序的过程中不断建立起类型变元之间的方程组如一个函数的形参类型和实参类型必须相等由此就可以得到一个新的方程并不断简化这些方程直到所有类型变元都可以求解出来或者缺乏足够的信息来求解此时就会将这样的类型变元泛化不过这超出本文的讨论范围了类型推断的过程十分类似于数学上解方程的过程。
这种做法的好处是这些方程组是从整个程序里所有信息中建立起来的所以每个未知类型都可以利用全局信息去求解解出的结果也可以保证是全局正确的。
例如下面这个程序在 Rust 中是可以编译通过的它可以根据第 5 行的函数调用解出变量 v 需要有 u16 类型。但是等价的程序在一些没有全局的类型推断的语言中则无法通过编译因为在第 4 行中 v 的类型就已经被推断为整数字面量的默认类型了这通常是 u64。
fn f(x:u16) {}
fn main() {let v 1;f(v);
}
那么为什么不是所有语言都用这种基于合一unification的类型推断方式呢主要问题就出在子类关系上。
如果类型间不存在子类关系那么所有类型实际上是一些离散的点两个类型要么相等要么不等几乎没有歧义的空间。这样求解方程非常简单直接结果也很容易保证完备性和可靠性。
但是有了子类关系类型之间就不再是一些毫无关系的点了而是形成了一个偏序集。从程序中可以建立起的也不再是基于类型相等的方程组而是基于子类关系的不等式组。求解一个偏序集上的不等式组则是一个复杂得多的问题很多时候我们甚至无法在可接受的时间内求得一个完全精确的解只能退而求其次做一些近似。这就导致基于合一unification的类型推断在有子类关系的语言中非常难以使用而仓颉语言是有子类关系的所以也暂时没有采用这种类型推断方式。 四、局部类型推断
上面讲的的子类关系会导致的问题曾一度导致在有子类关系的语言中做类型推断的研究非常稀少。对于注重实用的工业语言来说比较重要的一篇研究论文是 Benjamin. C. Pierce 等人著的 《Local Type Inference》1。它不再纠结于全局的完全性和完备性退而求其次只追求每个表达式的类型在相邻表达式能提供的信息中保证正确。仓颉的类型推断基本上是基于这篇论文的框架在实现。
更准确地来说《Local Type Inference》这篇论文实际上包含了两个类型推断的思想一个是仅依据局部信息做类型推断也就是“局部类型推断”另一个是类型信息应该在表达式中自底向上和自顶向下双向传播也叫“双向类型推断”。这两者在仓颉的类型推断实现中都有所体现下面就具体来介绍一下仓颉的类型推断方式
局部元素
在一个块内部编译器会按从上到下的顺序依次处理各个表达式和局部声明。
在一个表达式或局部声明的内部编译器依据可获得的类型信息会做自顶向下或者自底向上的推断。
自顶向下的推断是指父表达式如果对子表达式有期望的类型则我们会借助这个期望类型的信息去推断子表达式的类型。一个典型的情形是在一个函数调用表达式中我们总是期望实参的类型是对应位置形参的子类因而可以用形参类型作为期望类型去帮助推断实参类型。其他还包括 if 表达式的条件需要是 Bool 类型的子类变量的初始化表达式的类型需要是变量类型的子类等等。
下面举一些例子
func handleByte(b: Byte) {
}
func f() {let v: Int32 1 // 1 inferred to Int32handleByte(2) // 2 inferred to Byte
let v2 3 // 3 inferred to Int64
}
上面的程序中第5行的变量 v 有类型标注 Int32因此对其初始化表达式存在期望类型 Int32所以整数字面量 1 被推断为类型 Int32。
第6行的 handleByte 函数有形参类型 Byte因此这里的调用表达式对它的实参就有期望类型 Byte所以整数字面量 2 被推断为类型 Byte。
以上都是自顶向下的推断发生的场景而第8行中则没有发生自顶向下的推断。变量 v2 没有标注类型所以字面量 3 就不具有任何从父表达式得到的期望类型只能被推断为整数字面量的默认类型 Int64。 需要注意的是自顶向下的期望类型在一些表达式中是可以向下传递的。例如一个 if 表达式如果本身有期望类型那么我们会认为它的各个分支同样有这个期望类型。
下面是一个例子
func narrow(x: Int64):Byte {let v: Byte if (x 0) {1 // 1 inferred to Byte} else {-1 // -1 inferred to Byte}return v
}
其中变量 v 标注了类型 Byte因此其初始化表达式、即 if 表达式会具有期望类型 Byte。然后 if 的两个分支也都会传递地具有期望类型 Byte。因而第3行的 1 和第5行的 -1 字面量都将被推断为 Byte 类型。
除了 if 表达式以外一个表达式的返回值如果可能来源于它的某个子表达式那么对这个表达式的期望类型通常就可以传递给这个子表达式如从 match 表达式到它的各个 case从 try-catch 表达式到它的 try 分支和各个 catch 分支等等。
而自底向上的推断是指如果父表达式对子表达式没有期望的类型我们会先推断出子表达式的类型并反过来用这个信息帮助推断父表达式的类型。一个典型的场景是调用泛型函数时如果没有写出泛型参数则通常需要先推断出实参的类型然后才能依此求解出整个函数调用表达式的泛型参数进而得到整个表达式的类型。
以下是一个简单的例子
func idT(x: T): T {x
}
let s id(hello) // will infer idString
其中定义了一个接受一个任意类型的参数并返回其自身的泛型函数 id。第5行代码中我们既不知道变量 s 的类型也不知道调用的 id 函数的类型参数所以只能先从最里层的表达式 hello 开始推断得到它的类型为 String。然后向上利用实参类型为 String求解出此处调用 id 的泛型实参是 String进而确定它的返回类型也是 String最后再向上推断出变量 s 的类型是 String。 泛型参数求解
在调用泛型函数、或者构造泛型类型时我们需要知道本次调用的泛型实参。函数调用的泛型实参通常可以省略此时编译器会尝试从上下文中推断出泛型实参的类型。在局部类型推断中这是最为复杂的步骤也是唯一实际上用了合一unification的步骤。
上文介绍过在有子类关系的类型系统上合一unification需要求解不等式组。那么我们需要首先建立这些不等式。因为局部类型推断并不考虑全局信息所以针对一个特定的泛型函数的调用我们只会考虑下面几个不等式的来源 函数的形参类型需要是实参类型的父类 函数的返回类型需要是本次调用的期望返回类型的子类 函数的泛型约束需要被满足
具体求解的过程略为复杂本文不会详细介绍。大致上来说对于一个泛型参数编译器会尝试寻找能满足以上所有约束的唯一最具体类型、或唯一最抽象类型来作为这个泛型参数的解。如果这样的类型无法找到则会编译失败。另外如果找到的类型只能是 Any 或者 Nothing则编译也会失败。
以下是一个简单的情形
func tryPrintT(x: OptionT) where T : ToString {if (let Some(v) - x) {println(Has value: ${v})}
}
main() {tryPrint(Some(1)) // will infer tryPrintInt64
}
第8行代码中 tryPrint 函数的泛型参数需要推断。它的形参类型和实参类型间的对应关系为 OptionInt64 : OptionT此外它有泛型约束 T : ToString。结合两者我们发现类型 Int64可以作为 T 的解所以此处 tryPrint 的泛型实参就被推断为 Int64。
另外在一些较为复杂的情形下泛型函数的实参之间可能有类型信息的依赖无法用一次简单的自底向上或者自顶向下推断完成泛型参数的求解。这种情形在原版的《Local Type Inference》中并没有解决一个比较有名的后续工作叫做《Colored Local Type Inference》2它通过一个十分重量级的方法 -- 给类型中每个类型参数再更详细地标上需要自底向上还是自顶向下推断出来 -- 来实现对这种情形的支持。
仓颉参考了这种思路但是并没有引入那么重量级的标记只是会在泛型函数调用时尝试多次迭代求解泛型参数。以经典的 map 函数为例
import std.collection.ArrayList
func mapT, R(f: (T)-R, arg: ArrayListT): ArrayListR {let res ArrayListR()for (v in arg) {res.append(f(v))}res
}
main(){let input: ArrayListInt64 ArrayList([1, 2, 3])let output map({ x x.toString() }, input) // will infer mapInt64, String
}
map 函数接受一个转换函数和一个列表将列表中的元素逐一转换后输出新的列表。因为有转换前后两种不同类型所以它需要2个泛型参数 T 和 R。
在第13行对 map 的调用中泛型参数 T 可以很显然地从 input 参数的类型推断出来为 Int64但是对它的另一个参数即作为转换函数的 lambda在没有期望类型的情况下我们无法简单确定这个 lambda 的参数和返回类型因而也就无法解出 R 的类型。
但同时我们又可以观察到这个 lambda 的参数类型和 input 的类型都对应着泛型参数 T因此他们应该相等。而知道lambda的参数类型后他的返回类型就可以推断出来了。进而R 的类型也可以求解出来。
所以总的来说这种情形仍然是有足够的信息进行泛型参数的求解的只不过需要跨越参数进行一些类型信息的传递。
对于这种参数之间有类型信息的依赖的泛型函数调用我们的处理流程是这样的 首先推断出所有不需要期望类型就可以推断成功的实参的类型 然后用推断出的实参类型尽可能地求解泛型参数的类型 将可以求解出的泛型参数代入形参类型中将这些可能没有完全实例化的形参作为期望类型去推断对应的实参类型这个过程中我们会忽略掉类型中没有完全实例化的部分 重复 2、3 步直到没有新的泛型参数可以被求解即失败或者所有泛型参数都可以被求解即成功 最后还有一种较为特殊的场景有些函数可能定义成柯里化的形式即每次接收一个参数返回接收下一个参数的函数。
例如仓颉标准库中的 map 函数就提供了柯里化方式定义的版本
public func mapT, R(transform: (T) - R): (IterableT) - IteratorR {return {it: IterableT it.iterator().mapR(transform) }
}
柯里化的函数调用时会分为多次函数调用
let it map({xx.toString()})([1,2,3])
当然通常我们写成管道操作符的语法糖形式
let it [1, 2, 3] | map{xx.toString()}
这种情形下柯里化的泛型函数的多次调用是连续发生的它泛型参数仍然可以被推断出来编译器会将后面的调用中的实参类型信息以期望的返回类型的形式向前传播帮助推断泛型参数。
也就是说对于第一次对 map 的调用 map({xx.toString()})我们可以知道它的返回类型需要满足 (IterableT) - IteratorR : (ArrayInt64) - Any。然后使用上面描述过的求解步骤就可以解出 T 和 R 分别为 Int64 和 String。 重载决议
仓颉语言支持函数和操作符的重载在编译时需要静态地做重载决议以确定每个重载函数的调用究竟用了哪个定义。
仓颉做重载决议的过程大致上可以分为3步 找出当前调用位置可见的候选定义 检查每个候选定义是否能通过调用处局部的类型检查 在所有可以通过类型检查的定义中选取最匹配的一个
更具体的规则可以在用户手册或者语言规约中找到这里就不再赘述。这里主要讨论2个在重载决议过程中值得一提的点。
第一点是如果被调用函数的某些候选定义是泛型函数且需要求解泛型参数那么对每个候选定义会分别进行泛型参数的求解。 例如在下面的程序中第8行对 f 的调用若选取第1行的定义则可以求解出泛型参数 T 为 String若选取第4行的定义则可以求解出泛型参数 T 为 Int64。两者皆可类型检查通过所以会报错无法决议。
func fT(x: Int64, y: T) {
}func fT(x: T, y: String) {
}main() {f(1, c) // Error, both candidates match, ambiguous
}
第二点则是因为上面提到的双向类型推断而衍生出的问题。
因为我们采用的双向类型推断策略一个函数调用期望的返回类型对一个候选定义能否通过“局部的类型检查”会产生影响因而可能改变重载决议的结果。也就是说一个重载函数的调用在不同上下文下决议的结果是可能不同的。
例如下面的程序中第10行的 f 会考虑到期望的返回类型是 Int32 而选择第5行的定义而第11行的 f 会考虑到期望的返回类型是 Int64 而选择第1行的定义。
func f(x: Int64):Int64 {x
}func f(x: Int32):Int32 {x
}main() {let v1: Int32 f(1) // will use definition of line 5let v2: Int64 f(1) // will use definition of line 1
}
那么我们再考虑一种特殊的情况如果有多层重载函数的调用嵌套起来会发生什么事呢因为外层函数的形参会被视为内层函数调用的期望类型而外层函数的形参类型会依候选定义的选取而有所变化所以外层对候选定义的选取同样会影响内层的重载决议。
例如下面的程序中第10行外层的 widen 会考虑到期望的返回类型是 Int32 而选择第5行的定义而内层的 widen 会考虑到外层期望的参数类型是 Int16 而选择第1行的定义最后字面量 1 会因为第一行的 widen 定义期望一个 Int8 类型的参数而被推断为 Int8 类型。程序整体可以通过类型检查。
func widen(x: Int8):Int16 {Int16(x)
}func widen(x: Int16):Int32 {Int32(x)
}main() {let v: Int32 widen(widen(1)) // 1 inferred to Int8
}
这就产生了一个问题重载函数嵌套层数较多的情形下如比较大的UI组件、复杂的算术表达式等我们做决议可能需要搜索各层的候选组合而需要搜索的组合数可能随着嵌套层数而指数增长这就可能让编译时间长到无法接受。实际上同样的问题也可以在 Swift 语言中观察到例如至少在撰写本文时Swift 的编译器仍然会因为如下的程序编译超时
let a: Double -(1 2) -(3 4) -(5)
这和 Swift 同样使用了双向类型推断不无关系。
那么仓颉是如何解决这个问题的呢让我们回忆一下一个函数的重载决议总共需要哪些信息 当前的表达式 对当前表达式的期望类型 当前上下文中的符号表
其中对于源程序中同一个位置的表达式 1 是完全不变的3 可以近似认为不变事实上会导致指数的搜索量的是 2 在不同上下文中会有所不同。看到这里经常刷算法题的朋友可能可以敏锐地发现在双向类型推断下做重载决议实际上几乎是一个动态规划问题。对于给定的程序位置和期望类型只要上下文中的符号表不发生改变那么当前位置的表达式能否通过类型检查就是一个具有最优子结构的问题。而所有可能的期望类型并不是很多它最多等于父表达式调用的函数的候选定义的总数。
因此我们可以在重载决议时做一个记忆化搜索对同一个函数调用如果用同样的期望类型已经做过类型检查直接复用前一次检查时缓存的结果就好了。而在一些特殊情形下如果符号表确实发生了变化只要将受影响的缓存清除掉即可。如此一来对于绝大多数程序重载决议都可以在接近多项式的时间复杂度内完成。 六、小结
本文简单介绍了业界对类型系统和类型推断相关的讨论和已有工作并介绍了在仓颉的实践中类型推断遇到的问题和解决的方式。仓颉使用了基于局部类型推断的算法框架并针对一些常见的使用场景做了专门的优化在推断能力、算法复杂度、以及支持的语言特性间达到了一个不错的平衡点。 七、参考文献 [1] Pierce B C, Turner D N. Local type inference[J]. ACM Transactions on Programming Languages and Systems (TOPLAS), 2000, 22(1): 1-44. [2] Odersky M, Zenger C, Zenger M. Colored local type inference[J]. ACM SIGPLAN Notices, 2001, 36(3): 41-53.
