Motivation
Many developers favor statically typed languages like TypeScript, Rust, and Haskell for large-scale projects that demand correctness and reliability. However, as programming languages evolve to include advanced features such as structural typing, generics, and type inference, understanding and managing types can become increasingly hard. Writing simple programs often requires crafting intricate "essays of types," and navigating the convoluted types defined by third-party libraries can be even more challenging.
Modern editors and IDEs provide some level of type debugging support, including inline type hints and popover type signatures. Unfortunately, these tools fall short when a program is not well-typed, which is unfortunate since our code spends most of its time in the "ill-typed" state.
Goanna, an experimental type debugging tool for Haskell, aims to enhance the type debugging experience by offering deeper insights into type errors and suggesting clear paths to resolution.
Key Features
Precise Error Location
Goanna pinpoints all code fragments that contribute to type errors — not just a single location, as traditional compilers or standalone type checkers often do.
Fix type errors by traversing the multiverse
Goanna explores all potential solutions to fix type errors, leaving no stone unturned. For each suggested fix, the IDE predicts the resulting type assignments for the program, helping us understand the implications of our choices.
Type error isolation
If multiple type errors exist, Goanna catches them all, and reports each one separately. It intelligently detects related type errors and consolidates them into a single combined error, reducing the mental overhead for developers.
Type Inference for Untyped Expressions
Goanna can infer types for both typable and untypable expressions. For traditionally untyped expressions, it assigns them indeterminate types, whose type assignments depend on the programmer's path of action.
Our approach
Goanna employs its own constraint-based type inference engine rather than relying on the Hindley-Milner type system with algorithm W. In Goanna, Haskell source code is transformed into a constraint set, in the form of annotated ISO Prolog predicates. A Prolog engine then solves the generated constraints to determine the satisfiability of the constraint set, in other word, the type correctness of the program. To identify all potential fixes, Goanna explore Minimal Unsatisfiable Subsets (MUS) and Minimal Correction Subsets (MCS) within the constraint set, and perform a series of analyses base on the result. Each MCS corresponds to a possible fix, while MUS is used to perform type error isolation.