Structural and semantic pattern matching analysis in Haskell

TL;DR

This paper presents a static analysis tool for Haskell that improves detection of pattern matching issues by extending existing algorithms with SMT solver integration, enhancing precision and providing actionable warnings.

Contribution

It introduces an extended pattern matching analysis for Haskell that incorporates SMT solving to handle semantic constraints, improving detection accuracy over previous GHC implementations.

Findings

Enhanced detection of unmatched patterns and dead code.

Improved precision in static analysis through SMT solver integration.

Actionable warnings for Haskell program defects.

Abstract

Haskell functions are defined as a series of clauses consisting of patterns that are matched against the arguments in the order of definition. In case an input is not matched by any of the clauses, an error occurs. Therefore it is desirable to statically prove that the function is defined for all well-typed inputs. Conversely, a clause that can never be matched also indicates a likely defect. Analyzing these properties is challenging due to presence of GADT and guards as well as due to Haskell's lazy evaluation. We implement a recently proposed algorithm that unifies and extends the related analyses implemented in version 7 of the Glasgow Haskell Compiler. By using an SMT solver to handle the semantic constraints arising from pattern guards, we achieve a further improvement in precision over the existing GHC 8.0.1 implementation. We present a tool that uses the analysis to give sound, more precise, and actionable warnings about program defects.