GADTs and Exhaustiveness: Looking for the Impossible

Jacques Garrigue
(Nagoya University Graduate School of Mathematics)
Jacques Le Normand

Sound exhaustiveness checking of pattern-matching is an essential feature of functional programming languages, and OCaml supports it for GADTs. However this check is incomplete, in that it may fail to detect that a pattern can match no concrete value. In this paper we show that this problem is actually undecidable, but that we can strengthen the exhaustiveness and redundancy checks so that they cover more practical cases. The new algorithm relies on a clever modification of type inference for patterns.

In Jeremy Yallop and Damien Doligez: Proceedings ML Family / OCaml Users and Developers workshops (ML/OCaml 2015), Vancouver, Canada, 3rd & 4th September 2015, Electronic Proceedings in Theoretical Computer Science 241, pp. 23–35.
Published: 7th February 2017.

ArXived at: http://dx.doi.org/10.4204/EPTCS.241.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org