Content deleted Content added
m →Comparing declaration-site and use-site annotations: HTTP to HTTPS for Cornell University |
|||
| (48 intermediate revisions by 28 users not shown) | |||
Line 1:
{{Short description|Programming language concept}}
{{Type systems}}
Many [[programming language]] [[type system]]s support [[subtyping]]. For instance, if the [[type (computer science)|type]] {{C sharp|Cat}} is a subtype of {{C sharp|Animal}}, then an [[expression (computer science)|expression]] of type {{C sharp|Cat}} [[Liskov_substitution_principle|should be substitutable]] wherever an expression of type {{C sharp|Animal}} is used.
'''Variance'''
Depending on the variance of the [[type constructor]], the subtyping relation of the simple types may be either preserved, reversed, or ignored for the respective complex types. In the [[OCaml]] programming language, for example, "list of Cat" is a subtype of "list of Animal" because the list type constructor is '''covariant'''. This means that the subtyping relation of the simple types
On the other hand, "function from Animal to String" is a subtype of "function from Cat to String" because the function type constructor is '''contravariant''' in the [[parameter (computer science)|parameter]] type. Here, the subtyping relation of the simple types is reversed for the complex types.
A programming language designer will consider variance when devising [[typing
In order to keep the type system simple and allow useful programs, a language may treat a type constructor as invariant even if it would be safe to consider it variant, or treat it as covariant even though that could violate type safety.
== Formal definition ==
{{More citations needed section|date=November 2021}}
Within the [[type system]] of a [[programming language]], a typing rule or a type constructor is:▼
Suppose <code>A</code> and <code>B</code> are types, and <code><nowiki>I<U></nowiki></code> denotes application of a [[type constructor]] <code>I</code> with type argument <code>U</code>.
▲Within the [[type system]] of a
* ''covariant'' if it preserves the [[subtyping|ordering of types (≤)]], which orders types from more specific to more generic: If <code>A ≤ B</code>, then <code>I<nowiki><A> ≤ I<B></nowiki></code>;
* ''contravariant'' if it reverses this ordering: If <code>A ≤ B</code>, then <code>I<nowiki><B> ≤ I<A></nowiki></code>;
* ''bivariant'' if both of these apply (i.e., if <code>A ≤ B</code>, then <code>I<nowiki><A> ≡ I<B></nowiki></code>);
* ''variant'' if covariant, contravariant or bivariant;
* ''invariant'' or ''nonvariant'' if not variant.
Line 27 ⟶ 30:
* {{C sharp|Action<Animal>}} is a subtype of {{C sharp|Action<Cat>}}. The subtyping is reversed because {{C sharp|Action<T>}} is '''contravariant''' on {{C sharp|T}}.
* Neither {{C sharp|IList<Cat>}} nor {{C sharp|IList<Animal>}} is a subtype of the other, because {{C sharp|IList<T>}} is '''invariant''' on {{C sharp|T}}.
The variance of a C# generic interface is declared by placing the {{C sharp|out}} (covariant) or {{C sharp|in}} (contravariant) attribute on (zero or more of) its type parameters.<ref
The [[#Interfaces|typing rules for interface variance]] ensure type safety. For example, an {{C sharp|Action<T>}} represents a first-class function expecting an argument of type {{C sharp|T}},<ref name=Skeet />{{rp|144}} and a function that can handle any type of animal can always be used instead of one that can only handle cats.
== Arrays ==
Line 39 ⟶ 42:
* invariant: an {{java|Animal[]}} is not a {{java|Cat[]}} and a {{java|Cat[]}} is not an {{java|Animal[]}}.
If we wish to avoid type errors, then only the third choice is safe. Clearly, not every {{java|Animal[]}} can be treated as if it were a {{java|Cat[]}}, since a client reading from the array will expect a {{java|Cat}}, but an {{java|Animal[]}} may contain e.g. a {{java|Dog}}. So, the contravariant rule is not safe.
Conversely, a {{java|Cat[]}} cannot be treated as an {{java|Animal[]}}. It should always be possible to put a {{java|Dog}} into an {{java|Animal[]}}. With covariant arrays this cannot be guaranteed to be safe, since the backing store might actually be an array of cats. So, the covariant rule is also not safe—the array constructor should be ''invariant''. Note that this is only an issue for mutable arrays; the covariant rule is safe for immutable (read-only) arrays. Likewise, the contravariant rule would be safe for write-only arrays.
=== Covariant arrays in Java and C# ===
Line 61:
For instance, in Java {{java|String[]}} is a subtype of {{java|Object[]}}, and in C# {{C sharp|string[]}} is a subtype of {{C sharp|object[]}}.
As discussed above, covariant arrays lead to problems with writes into the array. Java<ref name=Bloch>{{cite book | title= "Effective Java: Programming Language Guide" |last=Bloch| first=Joshua| publisher=Addison-Wesley | edition=third | isbn=978-0134685991| year=2018}}</ref>{{rp|126}} and C# deal with this by marking each array object with a type when it is created. Each time a value is stored into an array, the execution environment will check that the run-time type of the value is equal to the run-time type of the array. If there is a mismatch, an {{java|ArrayStoreException}} (Java)<ref name=Bloch />{{rp|126}} or {{C sharp|ArrayTypeMismatchException}} (C#) is thrown:
<syntaxhighlight lang="java">
Line 70:
Object[] b = a;
// Assign an Integer (int) to b. This would be possible if b
// an array of Object, but since it really is an array of String,
// we will get a java.lang.ArrayStoreException at runtime.
b[0] = 1;
</syntaxhighlight>
Line 80:
One drawback to this approach is that it leaves the possibility of a run-time error that a stricter type system could have caught at compile-time. Also, it hurts performance because each write into an array requires an additional run-time check.
With the addition of generics, Java<ref name=Bloch />{{rp|126-129}} and C# now offer ways to write this kind of polymorphic function without relying on covariance. The array comparison and shuffling functions can be given the parameterized types
<syntaxhighlight lang="java">
Line 87:
</syntaxhighlight>
Alternatively, to enforce that a C# method accesses a collection in a read-only way, one can use the interface
== Function types ==
Languages with [[first-class function]]s have [[function type]]s like "a function expecting a Cat and returning an Animal" (written {{OCaml|
Those languages also need to specify when one function type is a subtype of another—that is, when it is safe to use a function of one type in a context that expects a function of a different type.
It is safe to substitute a function ''f'' for a function ''g'' if ''f'' accepts a more general type of argument and returns a more specific type than ''g''. For example, functions of type {{OCaml|
:<math>(P_1 \rightarrow R_1) \leq (P_2 \rightarrow R_2)</math> if <math>P_1 \geq P_2</math> and <math>R_1 \leq R_2</math>.
Line 106:
{{cite conference |first=Luca |last=Cardelli |title=A semantics of multiple inheritance |conference=Semantics of Data Types (International Symposium Sophia-Antipolis, France, June 27–29, 1984) |year=1984 |url=http://lucacardelli.name/Papers/Inheritance%20(Semantics%20of%20Data%20Types).pdf |series=Lecture Notes in Computer Science |volume=173 |publisher=Springer |pages=51–67 |isbn=3-540-13346-1 |doi=10.1007/3-540-13346-1_2}}<br/>Longer version: {{cite journal |author-mask=1 |first=Luca |last=Cardelli |title=A semantics of multiple inheritance |journal=Information and Computation |volume=76 |issue=2/3 |pages=138–164 |date=February 1988 |doi=10.1016/0890-5401(88)90007-7 |citeseerx=10.1.1.116.1298}}</ref>
When dealing with [[Higher-order function|functions that take functions as arguments]], this rule can be applied several times. For example, by applying the rule twice, we see that <math>((P_1 \to R) \to R) \le ((P_2 \to R) \to R)</math> if <math>P_1 \le P_2</math>. In other words, the type <math>((A \to B) \to C)</math> is ''covariant'' in the position of <math>A</math>. For complicated types it can be confusing to mentally trace why a given type specialization is or isn't type-safe, but it is easy to calculate which positions are co- and contravariant: a position is covariant if it is on the left side of an even number of arrows applying to it.
== Inheritance in object-oriented languages ==
When a subclass [[Method overriding|overrides]] a method in a superclass, the compiler must check that the overriding method has the right type. While some languages require that the type exactly matches the type in the superclass (invariance), it is also type safe to allow the overriding method to have a "better" type. By the usual subtyping rule for function types, this means that the overriding method should return a more specific type (return type covariance)
<gallery perrow="5" heights="190" caption="Variance and method overriding: overview">
Line 168:
</syntaxhighlight>
However, [[Sather]] supported both covariance and contravariance. Calling convention for overridden methods are covariant with ''out'' parameters and return values, and contravariant with normal parameters (with the mode ''in'').
Line 187:
</syntaxhighlight>
This is not type safe. By up-casting a {{java|CatShelter}} to an {{java|AnimalShelter}}, one can try to place a dog in a cat shelter. That does not meet {{java|CatShelter}} parameter restrictions
Despite the type safety problem, the Eiffel designers consider covariant parameter types crucial for modeling real world requirements.<ref name="competentCompilers"/> The cat shelter illustrates a common phenomenon: it is ''a kind of'' animal shelter but has ''additional restrictions'', and it seems reasonable to use inheritance and restricted parameter types to model this. In proposing this use of inheritance, the Eiffel designers reject the [[Liskov substitution principle]], which states that objects of subclasses should always be less restricted than objects of their superclass.
Line 296 ⟶ 295:
Another language feature that can help is ''multiple dispatch''. One reason that binary methods are awkward to write is that in a call like {{java|a.compareTo(b)}}, selecting the correct implementation of {{java|compareTo}} really depends on the runtime type of both {{java|a}} and {{java|b}}, but in a conventional OO language only the runtime type of {{java|a}} is taken into account. In a language with [[Common Lisp Object System]] (CLOS)-style [[multiple dispatch]], the comparison method could be written as a generic function where both arguments are used for method selection.
Giuseppe Castagna<ref>{{cite journal |first=Giuseppe |last=Castagna |title=Covariance and contravariance: conflict without a cause |journal=ACM Transactions on Programming Languages and Systems |volume=17 |issue=3 |pages=431–447 |date=May 1995 |doi=10.1145/203095.203096 |citeseerx=10.1.1.115.5992|s2cid=15402223 }}</ref> observed that in a typed language with multiple dispatch, a generic function can have some parameters which control dispatch and some "left-over" parameters which do not. Because the method selection rule chooses the most specific applicable method, if a method overrides another method, then the overriding method will have more specific types for the controlling parameters. On the other hand, to ensure type safety the language still must require the left-over parameters to be at least as general. Using the previous terminology, types used for runtime method selection are covariant while types not used for runtime method selection of the method are contravariant. Conventional single-dispatch languages like Java also obey this rule: only one argument is used for method selection (the receiver object, passed along to a method as the hidden argument {{java|this}}), and indeed the type of {{java|this}} is more specialized inside overriding methods than in the superclass.
Castagna suggests that examples where covariant parameter types are superior (particularly, binary methods) should be handled using multiple dispatch; which is naturally covariant.
Line 302 ⟶ 301:
=== Summary of variance and inheritance ===
{{uncited section|date=June 2024}}
The following table summarizes the rules for overriding methods in the languages discussed above.
Line 308:
! !! Parameter type !! Return type
|-
| [[C++]] (since 1998), [[Java (programming language)|Java]] (since [[Java Platform, Standard Edition|J2SE 5.0]]), [[D (programming language)|D]], [[C Sharp (programming language)|C#]] (since C# 9) || Invariant || Covariant
|-
| [[C Sharp (programming language)|C#]]
|-
|
|-
| [[Eiffel (programming language)|Eiffel]] || Covariant || Covariant
Line 378:
First, class members that have a variant type must be immutable. Here, <syntaxhighlight lang="scala" inline>head</syntaxhighlight> has the type <syntaxhighlight lang="scala" inline>A</syntaxhighlight>, which was declared covariant (<syntaxhighlight lang="scala" inline>+</syntaxhighlight>), and indeed <syntaxhighlight lang="scala" inline>head</syntaxhighlight> was declared as a method (<syntaxhighlight lang="scala" inline>def</syntaxhighlight>). Trying to declare it as a mutable field (<syntaxhighlight lang="scala" inline>var</syntaxhighlight>) would be rejected as type error.
Second, even if a data structure is immutable, it will often have methods where the parameter type occurs contravariantly. For example, consider the method <syntaxhighlight lang="scala" inline>::</syntaxhighlight> which adds an element to the front of a list. (The implementation works by creating a new object of the similarly
<syntaxhighlight lang="scala">
Line 389:
==== Inferring variance ====
It is possible to design a type system where the compiler automatically infers the best possible variance annotations for all datatype parameters.<ref name="tamingCombining">{{cite conference |
For these reasons<ref>{{cite web|title=Covariance and Contravariance in C# Part Seven: Why Do We Need A Syntax At All? |first=Eric |last=Lippert |date=October 29, 2007 |access-date=16 August 2016
Line 426:
Use-site variance means the desired variance is indicated with an annotation at the specific site in the code where the type will be used. This gives users of a class more opportunities for subtyping without requiring the designer of the class to define multiple interfaces with different variance. Instead, at the point a generic type is instantiated to an actual parameterized type, the programmer can indicate that only a subset of its methods will be used. In effect, each definition of a generic class also makes available interfaces for the covariant and contravariant ''parts'' of that class.
Java provides use-site variance annotations through [[Wildcard (Java)|wildcards]], a restricted form of [[bounded quantification|bounded]] [[existential type]]s. A parameterized type can be instantiated by a wildcard {{java|?}} together with an upper or lower bound, e.g. {{java|List<? extends Animal>}} or {{java|List<? super Animal>}}. An unbounded wildcard like {{java|List<?>}} is equivalent to {{java|List<? extends Object>}}. Such a type represents {{java|List<X>}} for some unknown type {{java|X}} which satisfies the bound.<ref name=Bloch />{{rp|139}} For example, if {{java|l}} has type {{java|List<? extends Animal>}}, then the type checker will accept
<syntaxhighlight lang="java">
Line 442:
[[File:Java wildcard subtyping.svg|thumb|right|350px|Wildcard subtyping in Java can be visualized as a cube.]]
While non-wildcard parameterized types in Java are invariant (e.g. there is no subtyping relationship between {{java|List<Cat>}} and {{java|List<Animal>}}), wildcard types can be made more specific by specifying a tighter bound. For example, {{java|List<? extends Cat>}} is a subtype of {{java|List<? extends Animal>}}. This shows that wildcard types are ''covariant in their upper bounds'' (and also ''contravariant in their lower bounds''). In total, given a wildcard type like {{java|C<? extends T>}}, there are three ways to form a subtype: by specializing the class {{java|C}}, by specifying a tighter bound {{java|T}}, or by replacing the wildcard {{java|?}} with a specific type (see figure).<ref name=Bloch />{{rp|139}}
By applying two of the above three forms of subtyping, it becomes possible to, for example, pass an argument of type {{java|List<Cat>}} to a method expecting a {{java|List<? extends Animal>}}. This is the kind of expressiveness that results from covariant interface types. The type {{java|List<? extends Animal>}} acts as an interface type containing only the covariant methods of {{java|List<T>}}, but the implementer of {{java|List<T>}} did not have to define it ahead of time.
In the common case of a generic data structure {{C sharp|IList}}, covariant parameters are used for methods getting data out of the structure, and contravariant parameters for methods putting data into the structure. The mnemonic for Producer Extends, Consumer Super (PECS), from the book ''Effective Java'' by [[Joshua Bloch]] gives an easy way to remember when to use covariance and contravariance.<ref name=Bloch />{{rp|141}}
Wildcards are flexible, but there is a drawback. While use-site variance means that API designers need not consider variance of type parameters to interfaces, they must often instead use more complicated method signatures. A common example involves the {{Javadoc:SE|java/lang|Comparable}} interface.<ref name=Bloch />{{rp|66}} Suppose we want to write a function that finds the biggest element in a collection. The elements need to implement the {{java|compareTo}} method,<ref name=Bloch />{{rp|66}} so a first try might be
<syntaxhighlight lang="java">
Line 461:
The bounded wildcard {{java|? super T}} conveys the information that {{java|max}} calls only contravariant methods from the {{java|Comparable}} interface. This particular example is frustrating because ''all'' the methods in {{java|Comparable}} are contravariant, so that condition is trivially true. A declaration-site system could handle this example with less clutter by annotating only the definition of {{java|Comparable}}.
The {{java|max}} method can be changed even further by using an upper bounded wildcard for the method parameter:{{sfn|Bloch|2018|loc=Chapter §5 Item 31: Use bounded wildcards to increase API flexibility|pp=139-145}}
<syntaxhighlight lang="java">
<T extends Comparable<? super T>> T max(Collection<? extends T> coll);
</syntaxhighlight>
=== Comparing declaration-site and use-site annotations ===
Line 469 ⟶ 474:
In a declaration-site language, libraries must either expose less variance, or define more interfaces. For example, the Scala Collections library defines three separate interfaces for classes which employ covariance: a covariant base interface containing common methods, an invariant mutable version which adds side-effecting methods, and a covariant immutable version which may specialize the inherited implementations to exploit structural sharing.<ref>{{cite web|title=The Scala 2.8 Collections API |first1=Marin |last1=Odersky |first2=Lex |last2=Spoon |date=September 7, 2010 |access-date=16 August 2016 |url=http://www.scala-lang.org/docu/files/collections-api/collections.html}}</ref> This design works well with declaration-site annotations, but the large number of interfaces carry a complexity cost for clients of the library. And modifying the library interface may not be an option—in particular, one goal when adding generics to Java was to maintain binary backwards compatibility.
On the other hand, Java wildcards are themselves complex. In a conference presentation<ref>{{cite web |first=Joshua |last=Bloch |title=The Closures Controversy [video] |date=November 2007 |place=Presentation at Javapolis'07 |url=http://parleys.com/play/514892250364bc17fc56bb15/chapter0/about |url-status=dead |archive-url=https://web.archive.org/web/20140202190630/http://parleys.com/play/514892250364bc17fc56bb15/chapter0/about |archive-date=2014-02-02 }}</ref> [[Joshua Bloch]] criticized them as being too hard to understand and use, stating that when adding support for [[Closure (computer science)|closures]] "we simply cannot afford another ''wildcards''". Early versions of Scala used use-site variance annotations but programmers found them difficult to use in practice, while declaration-site annotations were found to be very helpful when designing classes.<ref>{{cite conference |first1=Martin |last1=Odersky |first2=Matthias |last2=Zenger |title=Scalable component abstractions |book-title=Proceedings of the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA '05) |year=2005 |url=http://lampwww.epfl.ch/~odersky/papers/ScalableComponent.pdf |publisher=ACM |isbn=1595930310 |pages=41–57 |doi=10.1145/1094811.1094815 |citeseerx=10.1.1.176.5313}}</ref> Later versions of Scala added Java-style existential types and wildcards; however, according to [[Martin Odersky]], if there were no need for interoperability with Java then these would probably not have been included.<ref>{{cite web|title=The Purpose of Scala's Type System: A Conversation with Martin Odersky, Part III |
Ross Tate argues<ref name="MixedSiteVariance">{{cite conference |first=Ross |last=Tate |title=Mixed-Site Variance |book-title=FOOL '13: Informal Proceedings of the 20th International Workshop on Foundations of Object-Oriented Languages |year=2013 |url=
{{cite conference |
Since wildcards are a form of existential types they can be used for more things than just variance. A type like {{java|List<?>}} ("a list of unknown type"<ref>{{cite web |url=https://docs.oracle.com/javase/tutorial/java/generics/unboundedWildcards.html |title=The Java™ Tutorials, Generics (Updated), Unbounded Wildcards |access-date=July 17, 2020}}</ref>) lets objects be passed to methods or stored in fields without exactly specifying their type parameters. This is particularly valuable for classes such as {{Javadoc:SE|java/lang|Class}} where most of the methods do not mention the type parameter.
However, [[type inference]] for existential types is a difficult problem. For the compiler implementer, Java wildcards raise issues with type checker termination, type argument inference, and ambiguous programs.<ref>{{cite conference|title=Taming wildcards in Java's type system |first1=Ross |last1=Tate |first2=Alan |last2=Leung |first3=Sorin |last3=Lerner |book-title=Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation (PLDI '11) |year=2011 |url=
method List.add (capture#1) is not applicable
Line 490 ⟶ 495:
== See also ==
* [[Polymorphism (computer science)]]
* [[Inheritance (
* [[Liskov substitution principle]]
== Notes ==
{{notefoot}}
== References ==
| |||