WG211/M10Smaragdakis

Template Systems for Languages of the Future, Part III: Variance by Yannis Smaragdakis, based on "Taming the Wildcards: Combining Definition- and Use-Site Variance" (PLDI'11)

In a continuation of our recent work on advanced type systems for
templates/generics (MorphJ, cJ), I'll talk about the topic of variance.
"Variance" is the name for language mechanisms that integrate parametric
and subtype polymorphism, i.e., ask "when is a template instantiation a
subtype of another?". 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.