patternMinor
Covariance and Contravariance: Conflict without a Cause
Viewed 0 times
contravariancewithoutcovarianceconflictandcause
Problem
Here is the last paragraph at page 441 of the paper ‘Covariance and Contravariance: Conflict without a Cause’ by Giuseppe Castagna:
How is all this translated into object-oriented type systems? Consider a message $m$ applied (or “sent”) to $n$ objects $e_1$, …, $e_n$ where $e_i$ is an instance of class $C_i$. Suppose we want to consider the classes of only the first $k$ objects in the method selection process. This dispatching scheme can be expressed using the following notation:
$$m(e_1, …, e_k | e_{k+1}, …, e_n).$$
If the type of $m$ is $\{S_i → T_i\}_i$, then the expression above means that we want to select the method whose input type is the $\text{min}_i \{S_i | (C_1 × … × C_k) ≤ S_i\}$ and then to pass it all the $n$ arguments. The type, say $S_j → T_j$, of the selected branch must have the following form:
$$\underbrace{(A_1 × … × A_k)}_{S_j} → \underbrace{(A_{k+1} × … × A_n) → U}_{T_j}$$
where $C_i ≤ A_i$ for $1 ≤ i ≤ k$ and $A_i ≤ C_i$ for $k < i ≤ n$. If we want to override the selected branch by a more precise one, then, as explained above, the new method must covariantly override $A_1, …, A_k$ (to specialize the branch) and contravariantly override $A_{k+1}, …, A_n$ (to have type safety).
I expected $C_i ≤ A_i$ for $1 ≤ i ≤ n$ (instead of $C_i ≤ A_i$ for $1 ≤ i ≤ k$ and $A_i ≤ C_i$ for $k < i ≤ n$), because the call $m(e_1, …, e_n)$ is not type safe if we allow some argument types to be greater than the parameter types of the selected method.
Am I misinterpreting the paragraph or did the author make a mistake?
How is all this translated into object-oriented type systems? Consider a message $m$ applied (or “sent”) to $n$ objects $e_1$, …, $e_n$ where $e_i$ is an instance of class $C_i$. Suppose we want to consider the classes of only the first $k$ objects in the method selection process. This dispatching scheme can be expressed using the following notation:
$$m(e_1, …, e_k | e_{k+1}, …, e_n).$$
If the type of $m$ is $\{S_i → T_i\}_i$, then the expression above means that we want to select the method whose input type is the $\text{min}_i \{S_i | (C_1 × … × C_k) ≤ S_i\}$ and then to pass it all the $n$ arguments. The type, say $S_j → T_j$, of the selected branch must have the following form:
$$\underbrace{(A_1 × … × A_k)}_{S_j} → \underbrace{(A_{k+1} × … × A_n) → U}_{T_j}$$
where $C_i ≤ A_i$ for $1 ≤ i ≤ k$ and $A_i ≤ C_i$ for $k < i ≤ n$. If we want to override the selected branch by a more precise one, then, as explained above, the new method must covariantly override $A_1, …, A_k$ (to specialize the branch) and contravariantly override $A_{k+1}, …, A_n$ (to have type safety).
I expected $C_i ≤ A_i$ for $1 ≤ i ≤ n$ (instead of $C_i ≤ A_i$ for $1 ≤ i ≤ k$ and $A_i ≤ C_i$ for $k < i ≤ n$), because the call $m(e_1, …, e_n)$ is not type safe if we allow some argument types to be greater than the parameter types of the selected method.
Am I misinterpreting the paragraph or did the author make a mistake?
Solution
Yes, it is an error. For an application as in the example the relation must be, of course, the one you wrote, that is, $C_i≤A_i$ for $1≤i≤n$. The important sentence, however, is the one that follows, namely
If we want to override the selected branch by a more precise one, thenthe new method must covariantly override $A_1,…,A_k$ (to specialize the branch) and contravariantly override $A_{k+1},…,A_n$ (to have type safety).
It is in that case that the relation I (wrongly) wrote for the application must hold. That is, if the overriding method is defined for parameters of type $C_1,...,C_n$, then $C_i≤A_i$ for $1≤i≤k$ and $A_i ≤ C_i$ for $k. That is just to say that the theory is correct while the explanation is not.
I would strongly suggest abandoning this paper and rather continue with its recent follow-up, since I have reframed the problem of covariance and contravariance in terms of a much more modern type theory and giving practical examples in Perl6: Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) (published in Logical Methods in Computer Science, vol. 16, n. 1, pag. 15:1―15:58, 2020, but the link above gives the latest revised version).
Hopefully, the paper above is much more accessible than my 27-year-old paper, since I wrote it for an audience of undergraduate CS students and all is explained using running code.
P.S. Since I continually revise the paper above, feedback is highly welcome.
If we want to override the selected branch by a more precise one, thenthe new method must covariantly override $A_1,…,A_k$ (to specialize the branch) and contravariantly override $A_{k+1},…,A_n$ (to have type safety).
It is in that case that the relation I (wrongly) wrote for the application must hold. That is, if the overriding method is defined for parameters of type $C_1,...,C_n$, then $C_i≤A_i$ for $1≤i≤k$ and $A_i ≤ C_i$ for $k. That is just to say that the theory is correct while the explanation is not.
I would strongly suggest abandoning this paper and rather continue with its recent follow-up, since I have reframed the problem of covariance and contravariance in terms of a much more modern type theory and giving practical examples in Perl6: Covariance and Contravariance: a fresh look at an old issue (a primer in advanced type systems for learning functional programmers) (published in Logical Methods in Computer Science, vol. 16, n. 1, pag. 15:1―15:58, 2020, but the link above gives the latest revised version).
Hopefully, the paper above is much more accessible than my 27-year-old paper, since I wrote it for an audience of undergraduate CS students and all is explained using running code.
P.S. Since I continually revise the paper above, feedback is highly welcome.
Context
StackExchange Computer Science Q#150816, answer score: 2
Revisions (0)
No revisions yet.