Binding time analysis for polymorphically typed higher order languages

Abstract

Binding time analysis is used to distinguish the variables in a program that will have a known value at a time when only some of the parameters to the program are given. This is used in partial evaluation and has been found to be essential for efficient self-application and thus compiler generation by self-application of a partial evaluator with respect to an interpreter. Until recently, works in binding time analysis have used first order untyped languages, but the last year have seen a few papers treating typed lambda-calculus and a paper that argues that projections (domain retracts) could be used to describe binding times in a first order typed functional language. This paper extends the latter to higher order polymorphically typed functional languages and addresses some practical aspects of implementing the analysis.