By Chieri Saito, Atsushi Igarashi, and Mirko Viroli. Journal of Functional Programming, 18(3):285-331, 2008.
An earlier version appeared in Proceedings of the 3rd Asian Symposium on Programming Languages and Systems (APLAS'05), Springer LNCS 3780, pages 161-177, Tsukuba, Japan, November 2005.
Family polymorphism has been proposed for object-oriented languages as a solution to supporting reusable yet type-safe mutually recursive classes. A key idea of family polymorphism is the notion of families, which are used to group mutually recursive classes. In the original proposal, due to the design decision that families are represented by objects, dependent types had to be introduced, resulting in a rather complex type system.
In this article, we propose a simpler solution of lightweight family polymorphism, based on the idea that families are represented by classes rather than objects. This change makes the type system significantly simpler without losing much expressive power of the language. Moreover, "family-polymorphic" methods now take a form of parametric methods; thus it is easy to apply method type argument inference as in Java 5.0. To rigorously show that our approach is safe, we formalize the set of language features on top of Featherweight Java and prove the type system is sound. An algorithm for type inference for family-polymorphic method invocations is also formalized and proved to be correct. Finally, a formal translation by erasure to Featherweight Java is presented; it is proved to preserve typing and execution results, showing that our new language features can be implemented in Java by simply extending the compiler.
$Date: 2008-04-26 14:48:52 +0900 (Sat, 26 Apr 2008) $