A systematic approach to deriving incremental type checkers (2020)

This paper presents a systematic method for deriving incremental type checkers from standard type system specifications. The authors, André Pacak, Sebastian Erdweg, and Tamás Szabó, argue that immediate feedback from static typing is crucial for programmers, which is why most integrated development environments (IDEs) implement some form of incremental type checking. However, existing methods are often too specialized and difficult to adapt to new type systems. The proposed approach involves compiling inference rules into Datalog, a restricted logic programming language that supports incremental solvers. A significant contribution of this work is the encoding of the infinite typing relation into a finite Datalog relation, facilitating efficient incremental updates. The authors have implemented this compiler within a domain-specific language (DSL) for type systems, demonstrating its capability to handle simple types, local type inference, operator overloading, universal types, and iso-recursive types. This research aims to enhance the adaptability and efficiency of type checking in programming languages.

- The paper introduces a systematic approach to derive incremental type checkers from type system specifications.

- It utilizes Datalog for compiling inference rules, allowing for efficient incremental updates.

- The method addresses the limitations of existing incremental type checking approaches, making it more adaptable to various type systems.

- The implementation supports multiple type features, including simple types and operator overloading.

- The research emphasizes the importance of immediate feedback in static typing for programming efficiency.