GADTs and Exhaustiveness: Looking for the Impossible
Programming Languages
2017-02-09 v1
Abstract
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.
Cite
@article{arxiv.1702.02281,
title = {GADTs and Exhaustiveness: Looking for the Impossible},
author = {Jacques Garrigue and Jacques Le Normand},
journal= {arXiv preprint arXiv:1702.02281},
year = {2017}
}
Comments
In Proceedings ML/OCaml 2015, arXiv:1702.01872