Content deleted Content added
mNo edit summary Tags: Reverted Visual edit: Switched |
m →Comparing declaration-site and use-site annotations: HTTP to HTTPS for Cornell University |
||
| (16 intermediate revisions by 8 users not shown) | |||
Line 3:
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''' is
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 is preserved for the complex types.
On the other hand, "function
A programming language designer will consider variance when devising [[typing rule]]s for language features such as [[Array (data type)|array]]s, [[Inheritance (object-oriented programming)|inheritance]], and [[generic datatype]]s. By making type constructors covariant or contravariant instead of '''invariant''', more programs will be accepted as well-typed. On the other hand, programmers often find contravariance unintuitive, and accurately tracking variance to avoid [[runtime errors|runtime type errors]] can lead to complex typing rules.
Line 19:
* ''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 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 71 ⟶ 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 88 ⟶ 87:
</syntaxhighlight>
Alternatively, to enforce that a C# method accesses a collection in a read-only way, one can use the interface
== Function types ==
Line 110 ⟶ 109:
== 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 169 ⟶ 168:
</syntaxhighlight>
Only a few object-oriented languages actually allow this (for example, [[Python (programming language)|Python]] when typechecked with [[mypy]]). C++, Java and most other languages that support [[Function overloading|overloading]] and/or [[Variable shadowing|shadowing]] would interpret this as a method with an overloaded or shadowed name.
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 188 ⟶ 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 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 312:
| [[C Sharp (programming language)|C#]] (before C# 9) || Invariant || Invariant
|-
|
|-
| [[Eiffel (programming language)|Eiffel]] || Covariant || Covariant
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 |first1=John |last1=Altidor |first2=Huang Shan |last2=Shan |first3=Yannis |last3=Smaragdakis |title=Taming the wildcards: combining definition- and use-site variance |book-title=Proceedings of the 32nd ACM SIGPLAN conference on Programming language design and implementation (PLDI'11)
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 476:
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 |first1=Bill |last1=Venners |first2=Frank |last2=Sommers |date=May 18, 2009 |access-date=16 August 2016 |url=http://www.artima.com/scalazine/articles/scalas_type_system.html}}</ref>
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 |first1=Atsushi |last1=Igarashi |first2=Mirko |last2=Viroli |title=On Variance-Based Subtyping for Parametric Types |book-title=Proceedings of the 16th European Conference on Object-Oriented Programming (ECOOP '02) |year=2002 |isbn=3-540-47993-7 |pages=441–469 |doi=10.1007/3-540-47993-7_19 |series=Lecture Notes in Computer Science |volume=2374 |citeseerx=10.1.1.66.450}}</ref><ref>{{cite conference |first1=Kresten Krab |last1=Thorup |first2=Mads |last2=Torgersen |title=Unifying Genericity: Combining the Benefits of Virtual Types and Parameterized Classes |book-title=Object-Oriented Programming (ECOOP '99)
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 497:
* [[Inheritance (object-oriented programming)]]
* [[Liskov substitution principle]]
== Notes ==
{{notefoot}}
== References ==
| |||