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.
To get the PDF file, click here.