Dead Code Elimination through Dependent Types

• Main Author: Hongwei Xi
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Published: Springer Verlag 1999
• Subjects: Haskell; DML
• Online Access: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.7391; http://www.ececs.uc.edu/~hwxi/academic/papers/padl99.ps

. 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 .