Sound and Complete Type Inference for a Systems Programming Language
Recent advances in the theory and practice of programming languages have resulted in modern languages and tools that provide certain correctness guarantees regarding the execution of programs. However, these advances have not been effectively applied to the construction of systems programs, the core components of a computer system. This paper endeavors to bridge this gap between modern language design and systems programming. Discussing the support for these features in existing languages, the challenges in combining these feature sets are identified along with a description of the approach toward solving this problem. A new type system designed for safe systems programming is also introduced in the paper which features a new mutability model that combines unboxed types with a consistent typing of mutability. The type system is provably sound, supports polymorphism, and eliminates the need for alias analysis to determine the immutability of a location. The mutability model is expressive enough to permit mutation of unboxed/stack locations, and at the same time guarantees that types are definitive about the mutability of every location across all aliases. Complete support for mutability introduces challenges for type inference at copy boundaries. A novel algorithm that infers principal types using a system of constrained types has been developed. This is a stable and complete type inference algorithm that infers both mutability and polymorphism in a systems programming language with copy compatibility.