CAREER: Making Type Error Debugging Work

University Of Louisiana At Lafayette, Lafayette LA

Investigators

Abstract

A type system is part of a programming language to catch programming errors. Encouraged by their success, modern programming languages increasingly employ ever more sophisticated type systems to provide guarantees about the safety and correctness of programs. To make type systems convenient to use, languages usually rely on type inference to automatically determine types, thus saving programmers from tedious and manual type annotations. When type inference fails to compute a program's type, the error messages produced by existing compilers are often imprecise and difficult to understand, making it hard for programmers to fix a program. The goal of this research is to make type systems more usable, and thereby to assist programmers in fixing errors quickly and reliably. The intellectual merits of this research are a series of techniques and theories for generating informative messages for fixing type errors in advanced type systems, and a unified representation of error reparation for integrating various debugging techniques. The developed techniques are driven by insights gained from a large-scale empirical study and a usability study. The project's broader significance and importance is to make languages with advanced type systems and type inference more usable, leading to improved programming productivity and increased adoption of languages for constructing more reliable software. A reduced learning curve will specifically increase the adoption of such languages in both K-12 and higher education. The conceptual and technical development of the proposed research is backed by variational typing, a typing discipline that supports the reuse of computations, and that encodes type uncertainties with sound underlying theories and efficient implementations. The ability to reuse type information allows efficient exploration of large spaces of potential error fixes, the efficient location of errors, and the generation of informative error messages. While the proposed research targets Haskell, a type system laboratory with numerous advanced features, the techniques and theories developed by systematically studying the interactions of variational types and other typing features are applicable to a wide range of programming languages.