Home

GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness

GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness by Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, Simon Peyton Jones:

For ML and Haskell, accurate warnings when a function definition has redundant or missing patterns are mission critical. But today’s compilers generate bogus warnings when the programmer uses guards (even simple ones), GADTs, pattern guards, or view patterns. We give the first algorithm that handles all these cases in a single, uniform framework, together with an implementation in GHC, and evidence of its utility in practice.

Another great paper on a very useful incremental improvement on GADTs as found in Haskell, OCaml and Idris. Exhaustiveness checking is critical for a type system's effectiveness, and the redundant matching warnings are a nice bonus.

By naasking at 2015-10-10 02:37 | Admin | other blogs | 23016 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

How does this compare to Garrigue's paper...

... on a similar topic?

http://www.math.nagoya-u.ac.jp/~garrigue/papers/gadtspm.pdf

By yminsky at Wed, 2015-10-14 02:42 | login or register to post comments

Interesting that the

Interesting that the citations of both papers hardly overlap at all. Section 8.3 of the Haskell paper says OCaml's GADT checker does not warn of redundant cases, which is confirmed in the OCaml paper as well (although this extension is possible, and described in the paper). The OCaml algorithm is newer than the one cited by the Haskell paper though. I think the Haskell paper's take on the state of the art is still correct though, as described in section 2:

The question of determining exhaustiveness and redundancy of pattern matching has been well studied (Section 8), but almost exclusively in the context of purely structural matching. In this section we identify three new challenges:
• The challenge of GADTs and, more generally, of patterns that bind arbitrary existential type variables and constraints (Section 2.2).
• The challenge of laziness (Section 2.3).
• The challenge of guards (Section 2.4).
These issues are all addressed individually in the literature but, to our knowledge, we are the first to tackle all three in a single unified framework, and implement the unified algorithm in a production compiler.

By naasking at Wed, 2015-10-14 15:30 | login or register to post comments