Metacircularity in the polymorphic [lambda]-calculus

Abstract: "We consider the question of whether a useful notion of metacircularity existis for the polymorphic [lambda]-calculus. Even though complete metacircularity seems to be impossible, we obtain a close approximation to a metacircular interpreter. We begin by presenting an encoding for the Girard-Reynolds second-order polymorphic [lambda]-calculus in the third-order polymorphic [lambda]-calculus. The encoding makes use of representations in which abstractions are represented by abstractions, thus eliminating the need for the explicit representation of environments. We then extend this construction to encompass all of the [omega]-order polymorphic [lambda]-calculus (F[subscript [omega]]).The representation has the property that evaluation is definiable, and furthermore that only well-typed terms can be represented and thus type inference does not have to be explicitly defined. Unfortunately, this metacircularity result seems to fall short of providing a useful framework for typed metaprogramming. We speculate on the reasons for this failure and the prospects for overcoming it in the future. In addition, we briefly describe our efforts in designing a practical programming language based on F[subscript [omega]]."