While the focus of our language work at LogicBlox is on LogiQL, a declarative query language, we do, together with our academic collaborators, continue to contribute to the world of traditional imperative languages, as well. LogicBlox team member Shan Shan Huang, together with academic collaborators Yannis Smaragdakis and student John Altidor, published their most recent work on simplifying Java variance annotations in PLDI 2011. The paper discusses how to combine to different styles of variance, definition-site and use-site, to improve the ease of use without sacrificing type safty.
Abstract Variance allows the safe integration of parametric and subtype polymorphism. Two flavors of variance, definition-site versus use-site variance, have been studied and have had their merits hotly debated. Definition-site variance (as in Scala and C#) offers simple type-instantiation rules, but causes fractured definitions of naturally invariant classes; Use-site variance (as in Java) offers simplicity in class definitions, yet complex type-instantiation rules that elude most programmers. We present a unifying framework for reasoning about variance. Our framework is quite simple and entirely denotational, that is, it evokes directly the definition of variance with a small core calculus that does not depend on specific type systems. This general framework can have multiple applications to combine the best of both worlds: for instance, it can be used to add use-site variance annotations to the Scala type system. We show one such application in detail: we extend the Java type system with a mechanism that modularly infers the definition-site variance of type parameters, while allowing use-site variance annotations on any type-instantiation. Applying our technique to six Java generic libraries (including the Java core library) shows that 20-58% (depending on the library) of generic definitions are inferred to have single-variance; 8-63% of method signatures can be relaxed through this inference, and up to 91% of existing wildcard annotations are unnecessary and can be elided.