Finitary polymorphism for optimizing type-directed compilation
Finitary polymorphism for optimizing type-directed compilation
复制标题
用于优化类型定向编译的有限多态性
DOI：
10.1145/3236776
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Hisayuki Mima
中科院分区：
文献类型：
--
作者：
Atsushi Ohori;Katsuhiro Ueno;Hisayuki Mima
我们提出了一种类型理论方法来优化多态语言的类型定向编译，并在SML#中实现了该方法，SML#是标准ML的全面编译器，扩展了几个需要类型传递操作语义的高级功能，并通过性能评估报告了该方法的有效性。为此，我们首先定义了具有有限多态的谓词二阶Lambda演算，其中每个类型抽象被显式地约束到有限类型宇宙，并建立关于类型传递操作语义的类型可靠性。与具有分层类型宇宙的微积分不同，该微积分的类型宇宙是表示实例类型的有限集合的术语。然后，我们开发了一种宇宙重建算法，该算法取标准二阶Lambda演算中的一项，检查该项是否可用有限多态来类型化，如果可类型化，则在有限多态演算中构造一个项。基于这些结果，我们提出了一种基于类型的多态函数优化方法。因为我们的形式主义是基于二阶Lambda演算的，所以它可以用来优化各种多态语言。我们实现了原生(无标签)数据表示和记录多态的优化方法，并通过基准测试评估了其有效性。测试表明，消除了83.79%的类型传递抽象，实现了编译代码平均15.28%的加速。
We develop a type-theoretical method for optimizing type directed compilation of polymorphic languages, implement the method in SML#, which is a full-scale compiler of Standard ML extended with several advanced features that require type-passing operational semantics, and report its effectiveness through performance evaluation. For this purpose, we first define a predicative second-order lambda calculus with finitary polymorphism, where each type abstraction is explicitly constrained to a finite type universe, and establishes the type soundness with respect to a type-passing operational semantics. Different from a calculus with stratified type universes, type universes of the calculus are terms that represent a finite set of instance types. We then develop a universe reconstruction algorithm that takes a term of the standard second-order lambda calculus, checks if the term is typable with finitary polymorphism, and, if typable, constructs a term in the calculus of finitary polymorphism. Based on these results, we present a type-based optimization method for polymorphic functions. Since our formalism is based on the second-order lambda calculus, it can be used to optimize various polymorphic languages. We implement the optimization method for native (tag-free) data representation and record polymorphism, and evaluate its effectiveness through benchmarks. The evaluation shows that 83.79% of type passing abstractions are eliminated, and achieves the average of 15.28% speed-up of compiled code.