The Essence of Lightweight Family Polymorphism.
2008; EtH Zurich; Volume: 7; Issue: 5 Linguagem: Inglês
10.5381/jot.2008.7.5.a3
ISSN1660-1769
AutoresChieri Saito, Atsushi Igarashi,
Tópico(s)Formal Methods in Verification
ResumoWe 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 only type declarations, from .FJ into FGJ self , an extension of Featherweight GJ with 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 FGJ self enjoys type soundness and the formal translation preserves typing and reduction.
Referência(s)