In the field of programming language theory, a type system is a formal system that categorises expressions into specific types in a compositional manner. A robust type system plays a crucial role in preventing certain undesirable program behaviours, thus enabling early detection of programming errors. By incorporating more features into their type systems, programming languages can achieve greater expressive capabilities. Nevertheless, the inclusion of new features into a type system may lead to increased metatheoretical complexity. Therefore, care must be taken when designing a type system.
Bounded quantification, which combines subtyping and parametric polymorphism, is a key feature in many modern programming languages, such as Java, Scala, and TypeScript. The concept of bounded quantification was initially introduced by Cardelli and Wegner in an experimental programming language called Fun. The type system of Fun was later refined and formalised into a calculus known as System F<: by Curien and Ghelli.
In System F<:, there are four kinds of types, namely the top type, variable types, function types, and universal types. The subtype relationship <: is a preorder on them.
While System F<: was widely adopted as the standard calculus for bounded quantification, it was eventually demonstrated to have an undecidable subtype relation. In other words, it is impossible to design a subtyping algorithm for System F<: that guarantees its termination.
The main focus of this project is thus to investigate the design of a mechanism for bounded quantification that guarantees its decidability. This involves proposing new inference rules and using a interactive theorem prover to verify their desirable properties, such as reflexivity, transitivity, and decidability. Subsequently, a toy programming language incorporating the revised type system will be implemented. The ultimate goal is to improve the usability of programming languages and increase the productivity of programmers.