By Chieri Saito and Atsushi Igarashi. Journal of Object Technology, 7(5):67-99, 2008. Special Issue: Workshop on FTfJP 2007.
A preliminary version appeared in Proceedings of the 9th Workshop on Formal Techniques for Java-like Programs (FTfJP 2007), pages 27-41, Berlin, Germany, July 2007.
We have proposed lightweight family polymorphism, a programming style to support reusable yet type-safe mutually recursive classes, and introduced its formal core calculus .FJ. In this paper, we give a formal translation, which changes \emph{only} type declarations, from .FJ into FGJself, an extension of Featherweight GJ with \emph{self type variables}. They improve self typing and are required for the translation to preserve typing. Therefore we claim that self type variables represent the essential difference between .FJ and Featherweight GJ, namely, lightweight family polymorphism provides better self typing for mutually recursive classes than Java generics. To support this claim rigorously, we show that FGJself enjoys type soundness and the formal translation preserves typing and reduction.
$Date: 2008-06-12 15:19:49 +0900 (Thu, 12 Jun 2008) $