A type-and-effect system for object initialization
A type-and-effect system for object initialization
复制标题
用于对象初始化的类型和效果系统
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Martin Odersky
中科院分区：
文献类型：
--
作者：
Fengyun Liu;Ondřej Lhoták;Aggelos Biboudis;Paolo G. Giarrusso;Martin Odersky
每个新创建的对象都会经历几个初始化状态：从所有字段都未初始化的状态开始，直到所有字段都被赋值。在初始化过程中对对象的任何操作，通常发生在构造函数中，必须观察对象的初始化状态以确保正确性，即只能使用初始化的字段。静态地检查它的安全使用，而不需要在源代码中手动注释初始化状态，这是一个挑战，因为它有别名和虚方法调用。主流语言要么不检查初始化错误，如Java、C++、Scala，要么通过不支持有用的初始化模式来防御它们，如Swift。与此同时，过去的研究表明，可以通过牺牲语法简单性来实现不同程度的表达能力的安全初始化。我们的方法的问题，坚持本地推理的初始化，避免了整个程序分析，我们实现了类型状态多态性通过子类型。在此基础上，我们提出了一种新的类型和效果的系统，可以有效地确保初始化的安全性，同时允许灵活的初始化模式。我们在Scala 3编译器中实现了一个初始化检查器，并在几个实际项目中进行了评估。
Every newly created object goes through several initialization states: starting from a state where all fields are uninitialized until all of them are assigned. Any operation on the object during its initialization process, which usually happens in the constructor via this, has to observe the initialization states of the object for correctness, i.e. only initialized fields may be used. Checking safe usage of this statically, without manual annotation of initialization states in the source code, is a challenge, due to aliasing and virtual method calls on this. Mainstream languages either do not check initialization errors, such as Java, C++, Scala, or they defend against them by not supporting useful initialization patterns, such as Swift. In parallel, past research has shown that safe initialization can be achieved for varying degrees of expressiveness but by sacrificing syntactic simplicity. We approach the problem by upholding local reasoning about initialization which avoids whole-program analysis, and we achieve typestate polymorphism via subtyping. On this basis, we put forward a novel type-and-effect system that can effectively ensure initialization safety while allowing flexible initialization patterns. We implement an initialization checker in the Scala 3 compiler and evaluate on several real-world projects.