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. © Springer-Verlag Berlin Heidelberg 1998.
CITATION STYLE
Xi, H. (1999). Dead code elimination through dependent types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1551 LNCS, pp. 228–242). https://doi.org/10.1007/3-540-49201-1_16
Mendeley helps you to discover research relevant for your work.