Phase Distinctions In The Compilation Of EPIGRAM
James McKinna, Edwin C. Brady · 2005
Abstract. It is commonly believed that in dependently typed programming languages, the blurring of the distinction between types and values means that no type erasure is possible at run-time. In this paper, however, we propose an alternative phase distinction. Rather than distinguishing types and values in the compilation of EPIGRAM, we distinguish compile-time and run-time evaluation, and show by a series of program transformations that values which are not required at run-time can be erased. 1