Modernizing SMT-Based Type Error Localization

TL;DR

Tyro is a novel SMT-based tool that improves type error localization in functional programming languages by using an intermediate representation and advanced SMT solving techniques, leading to more accurate and scalable error detection.

Contribution

Introduces Tyro, a modular SMT-based type error localization system with a new encoding for polymorphic types and an intermediate representation, enhancing accuracy and scalability.

Findings

Effective in identifying accurate error sources in ill-typed programs.

Scalable to larger programs with improved error localization.

Supports integration into programming environments for better user feedback.

Abstract

Traditional implementations of strongly-typed functional programming languages often miss the root cause of type errors. As a consequence, type error messages are often misleading and confusing - particularly for students learning such a language. We describe Tyro, a type error localization tool which determines the optimal source of an error for ill-typed programs following fundamental ideas by Pavlinovic et al. : we first translate typing constraints into SMT (Satisfiability Modulo Theories) using an intermediate representation which is more readable than the actual SMT encoding; during this phase we apply a new encoding for polymorphic types. Second, we translate our intermediate representation into an actual SMT encoding and take advantage of recent advancements in off-the-shelf SMT solvers to effectively find optimal error sources for ill-typed programs. Our design maintains the separation of heuristic and search also present in prior and similar work. In addition, our architecture design increases modularity, re-usability, and trust in the overall architecture using an intermediate representation to facilitate the safe generation of the SMT encoding. We believe this design principle will apply to many other tools that leverage SMT solvers. Our experimental evaluation reinforces that the SMT approach finds accurate error sources using both expert-labeled programs and an automated method for larger-scale analysis. Compared to prior work, Tyro lays the basis for large-scale evaluation of error localization techniques, which can be integrated into programming environments and enable us to understand the impact of precise error messages for students in practice.