Dead Code Elimination through Dependent Types
Dead Code Elimination through Dependent Types
复制标题
通过依赖类型消除死代码
DOI：
10.1007/3-540-49201-1_16
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
H. Xi
中科院分区：
文献类型：
--
作者：
H. Xi
模式匹配是各种函数式编程语言（如SML、Caml、Haskell等）的重要特性。在这些语言中，不可达或冗余的匹配子句可以被视为一种特殊形式的死代码，是程序错误的丰富来源。因此，在编译时消除不可达匹配子句可以显著增强程序错误检测。此外，这还可以在运行时显著提高代码的效率。
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 compile-time 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.