一句话：提出基于SVE的混合布尔合一算法并用于Flix，将类型与效应推断开销显著降低，编译吞吐提升1.8倍。
表达力更强的类型与效应系统对高效类型推断提出更高要求。本文面向基于布尔公式的多态效应系统，其推断需布尔合一；因涉及语义等价，语法驱动合一不足，已有布尔合一技术也不适合类型推断。作者提出基于 Boole 逐次变量消去（SVE）的混合算法，利用实际查询多为简单、灵活变量少、易重复且存在长尾复杂查询等特点，并结合 tabling 与二元决策图等公式最小化策略。该算法在 Flix 中实现，实验显示编译吞吐从 8,580 行/秒增至 15,917 行/秒（1.8 倍），类型与效应推断开销仅 16%，总编译开销低于 7%，各设计选择均提升性能。
As type and effect systems become more expressive there is an increasing need for efficient type inference. We consider a polymorphic effect system based on Boolean formulas where inference requires Boolean unification. Since Boolean unification involves semantic equivalence, conventional syntax-driven unification is insufficient. At the same time, existing Boolean unification techniques are ill-suited for type inference. We propose a hybrid algorithm for solving Boolean unification queries based on Boole’s Successive Variable Elimination (SVE) algorithm. The proposed approach builds on several key observations regarding the Boolean unification queries encountered in practice, including: (i) most queries are simple, (ii) most queries involve a few flexible variables, (iii) queries are likely to repeat due similar programming patterns, and (iv) there is a long tail of complex queries. We exploit these observations to implement several strategies for formula minimization, including ones based on tabling and binary decision diagrams. We implement the new hybrid approach in the Flix programming language. Experimental results show that by reducing the overhead of Boolean unification, the compilation throughput increases from 8,580 lines/sec to 15,917 lines/sec corresponding to a 1.8x speed-up. Further, the overhead on type and effect inference time is only 16% which corresponds to an overhead of less than 7% on total compilation time. We study the hybrid approach and demonstrate that each design choice improves performance.
@article{paperbot1872,
title = {Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems},
author = {Magnus Madsen and Jaco van de Pol and Troels Henriksen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622816}
}