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 un...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
Springer Verlag
1999
|
| Subjects: | |
| 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 |
| Summary: | . 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 . |
|---|