A Variation on Java Wildcards - Trading Expressiveness for Global Type Inference

Le résumé fourni par la source

In standard Java, wildcards behave like existential types: they must be opened before use in a method invocation, a process the compiler performs implicitly via capture conversion. We present Java-TX, a dialect of Java that sidesteps this existential encoding and treats wildcards as placeholders for unknown types, used directly without prior opening. This choice simplifies the type system and makes it compatible with an existing global type inference algorithm. The trade-off is that some method calls valid in standard Java become unavailable in Java-TX. In effect, we trade some of Java’s wildcard expressiveness for global type inference. We explore the metatheory of Java-TX through Featherweight Java-TX (FJ-TX), a functional core calculus for Java-TX that extends Featherweight Generic Java with our wildcard interpretation. We prove type soundness for FJ-TX. Finally, we evaluate the practical impact of omitting capture conversion by conducting a study on open-source Java projects by calculating an underapproximation of how much existing Java code is compatible with the Java-TX type system.

Ce résumé expose les affirmations des auteurs. BNTIC ne l’interprète pas comme une validation indépendante des résultats.