Name: Zhiping Cai
Date: Monday April 3rd 2023
Time: 3:00pm - 4:00pm (EST)
Location: EIT 3145
Supervisor: Prof. Werner Dietl
Attending faculty members: Prof. Arie Gurfinkel, and Prof. Mahesh Tripunitara
Title: UniFlow: A CFG-based Framework for Pluggable Type Checking andType Inference
Abstract:
Type system is a crucial component of high-level programming languages, as it enhances program correctness by ruling out certain type errors. For statically-typed languages, a compiler may implement a static type system by leveraging the existing type information. However, these built-in type systems often adhere to a specific set of rules defined by the language's specification (e.g., Java, Kotlin and C++). Pluggable type system was then introduced as an idea to provide customizable type rules for different scenarios.
Various approaches exist for implementing a pluggable type system. The Checker Framework is a well-known framework to facilitate the development of type checkers for Java. This framework enables developers to define their type rules and override the analysis logic. Additionally, Checker Framework Inference is a framework built upon the Checker Framework to provide constraint-based whole-program inference. It helps to reduce the burden of manually annotating the code base when applying a new type system.
However, the complexity of these frameworks presents a steep learning curve to type system developers. As the maintainers of these frameworks, we examine some of the critical issues encountered in our previous development experience. The Checker Framework performs its analysis on two different program representations: AST and CFG. The shared responsibilities of these representations in the framework cause readability and maintainability issues for developers. Checker Framework Inference suffers not only from the same problem but also from difficulty in employing the same type rules for type checking and type inference. This is because the underlying Checker Framework assumes a deterministic mechanism, while the constraint-based approach is non-deterministic in general.
We ropose a novel CFG-based type system framework, UniFlow, addressing the aforementioned issues by providing a unified development process for type systems supporting both type checking and type inference. It strives to resolve types and apply type rules on the program's CFGs whenever possible. This approach reduces friction in type system development, allowing developers to focus on a single flow-sensitive program representation that is simpler than ASTs. It also forces developers to express type rules as constraints, such that the same set of type rules can be implemented once, but consistently reused in type checking and type inference. Moreover, our framework supports running multiple type systems and attempts to improve error message reporting for users.
We present UniFlow's architecture and explain each crucial component and functionality in detail. We discuss the advantages and limitations of our framework. Furthermore, we share the initial implementation of the framework and outline future research directions.