We show a type-based method for useless variable elimination, i.e.,
transformation that eliminates variables whose values contribute
nothing to the final outcome of a computation, and prove its
correctness. The algorithm is a surprisingly simple extension of the
usual type reconstruction algorithm. Our method seems more attractive
than Wand and Siveroni's 0CFA-based method in many respects. First, it
is efficient: it runs in time almost linear in the size of an input
expression for a simply-typed lambda-calculus, while the 0CFA-based
method may require a cubic time. Second, our transformation can be
shown to be optimal among those that preserve well-typedness, both for
the simply-typed language and for an ML-style polymorphically-typed
language. On the other hand, the 0CFA-based method is not optimal for
the polymophically-typed language.