Dead Code Elimination through Dependent Types

Pattern matching is an important feature in various functional programming languages such as SML, Caml, Haskell, etc. In these languages, unreachable or redundant matching clauses, which can be regarded as a special form of dead code, are a rich source for program errors. Therefore, eliminating unreachable matching clauses at compiletime can significantly enhance program error detection. Furthermore, this can also lead to significantly more efficient code at run-time.We present a novel approach to eliminating unreachable matching clauses through the use of the dependent type system of DML, a functional programming language that enriches ML with a restricted form of dependent types. We then prove the correctness of the approach, which consists of the major technical contribution of the paper. In addition, we demonstrate the applicability of our approach to dead code elimination through some realistic examples. This constitutes a practical application of dependent types to functional programming, and in return it provides us with further support for the methodology adopted in our research on dependent types in practical programming.