We introduce and study Constraint-Bounded Polymorphism (CBP), an expressive type system for object-oriented languages. CBP advances constrained parametric polymorphism, under which declarations' type parameters can be restricted by imposing type constraints. Type constraints allow the programmer to express additional information and invariants about the code and can be checked at compile-time, reducing development time and likelihood of errors.
CBP defines subtype and signature constraints with inference-based constraint solving, and allows independent parameterization and constraining of type, subtype, signature, and method declarations. This provides, in a uniform framework, a variety of known and new type system features. The new features include conditional subtyping; the known features include F-bounded polymorphism, programmer-defined co- and contravariant type parameters, Theta-style where clauses, structural subtyping, union and intersection types, and constraint-based typing of expressions.
We give a formal definition of CBP and corresponding typechecking rules for a core host language, extending known approaches for constraint-based typing of expressions and typechecking of multi-methods. We establish type soundness. We provide a typechecking algorithm based on constraint solving, which is sound and terminating under certain restrictions on the structure of the source program's declarations.
We validate CBP on the Vortex research compiler infrastructure, a 100,000-line Cecil program. Originally Vortex developers had not been significantly restricted by a type system (taking advantage of typechecking being optional in Cecil). We had found several coding idioms in Vortex that were not amenable to being typechecked by existing type systems, which served as a motivation for this work. We then implemented CBP in Cecil and made Vortex pass the typechecker. Our experience was that the type system was able to support almost all of the coding idioms in Vortex, occasionally with minor changes to the code. Since then, Vortex developers have reported that the type system had supported them and reduced development time. A study of Vortex after several years of its development under the typechecking discipline shows that CBP's advanced features are important for achieving static type-correctness but are used in Vortex in only a few idiomatic ways.
Cited By
- Shvedenko V, Shvedenko V and Shchekochikhin O (2018). Using Structural Polymorphism in Creating Process-Based Management Information Systems, Automatic Documentation and Mathematical Linguistics, 52:6, (290-296), Online publication date: 1-Nov-2018.
- Zappa Nardelli F, Belyakova J, Pelenitsyn A, Chung B, Bezanson J and Vitek J (2018). Julia subtyping: a rational reconstruction, Proceedings of the ACM on Programming Languages, 2:OOPSLA, (1-27), Online publication date: 24-Oct-2018.
- Wehr S and Thiemann P (2011). JavaGI, ACM Transactions on Programming Languages and Systems (TOPLAS), 33:4, (1-83), Online publication date: 1-Jul-2011.
- Sedunov A and Tyukachev N An approach to modular object-oriented programming in language-driven development framework Proceedings of the 6th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems, (1-8)
Recommendations
Guarded impredicative polymorphism
PLDI 2018: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe design space for type systems that support impredicative instantiation is extremely complicated. One needs to strike a balance between expressiveness, simplicity for both the end programmer and the type system implementor, and how easily the system ...