Haskell meets Evariste

TL;DR

The paper tackles documentation ambiguity in functional libraries by advocating an easy-hard-split approach grounded in Galois connections. It uses takeWhile and zip from Haskell's Data.List as case studies to derive precise formal specifications from informal descriptions, showing how a prefix-based ordering and its generalization to sublists enable correct-by-construction implementations. The key contribution is a reusable framework that improves clarity and reuse across languages, with idempotent properties for patterns like takeWhile, filter, and dropWhile. The approach offers broad applicability to library design and formal reasoning in functional programming, paving the way for more reliable and maintainable software components.

Abstract

Since its birth as a new scientific body of knowledge in the late 1950s, computer programming has become a fundamental skill needed in many other disciplines. However, programming is not easy, it is prone to errors and code re-use is key for productivity. This calls for high-quality documentation in software libraries, which is quite often not the case. Taking a few Haskell functions available from the Hackage repository as case-studies, and comparing their descriptions with similar functions in other languages, this paper shows how clarity and good conceptual design can be achieved by following a so-called easy-hard-split formal strategy that is quite general and productive, even if used informally. This strategy is easy to use in functional programming and can be applied to both program analysis and synthesis.