Type-Based Useless Variable Elimination

Useless variable elimination [25] is a transformation that eliminates variables whose values contribute nothing to the final outcome of a computation. We present a type-based method for useless variable elimination and prove its correctness. The algorithm is a surprisingly simple extension of the usual type reconstruction algorithm. Our method seems more attractive than other methods for useless variable elimination in several respects. First, it is simple, so that the proof of the correctness is clear and the method can be easily extended to deal with a polymorphic language. Second, it is efficient: it runs in time almost linear in the size of an input expression for a simply-typed A-calculus, while Wand and Siveroniʹs OCFA-based method may require a cubic time. Moreover, our transformation is optimal in a certain sense among those that preserve well-typedness, both for the simply-typed language and for an ML-style polymorphically-typed language. On the other hand, Wand and Siveroniʹs method is not optimal for the polymophicallytyped language.