Home » forums » LtU Forum

Looking for papers on covariance and contravariance

Hello,

I am looking for papers and a particular paper I used to have on covariance and contravariance.

The paper I used to have many years ago probably about 2006 or 2007 when I originally started looking into type theory and did not realize its relevance had many inference rules for covariance and contravariance using plus and minus symbols within the inference rules.

I am now researching this area and am interested in any papers on this topic.

Many thanks in advance,

Aaron Gray

By AaronNGray at 2018-12-25 21:44 | LtU Forum | previous forum topic | next forum topic | other blogs | 3710 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

two by castagna

Two by Castagna:

2013: https://arxiv.org/pdf/1809.01427.pdf
1994: https://www.irif.fr/~gc/papers/toplas95.pdf

One thing I really dislike about academic papers is how hard it is to find the date.
However the important one is the original, which i can't find, which basically
destroys Object Orientation as way of representing abstract types, ,the famous "covariance problem". Bertrand Meyer also discovered this and had to add hacks to Eiffel to compensate, similar to C++ dynamic cast. There's also been a lot of rubbish about double dispatch, a type theorists version of a perpetual motion machine.

By skaller at Tue, 2019-01-01 15:19 | login or register to post comments

Plenty of people have done

Plenty of people have done contra and covariance in object oriented languages without trouble. Meyer didn't care, maybe he didn't know, but how many people are programming in Eiffel today anyways?

By Sean McDirmid at Fri, 2019-01-04 05:13 | login or register to post comments

Good papers

Those are good, particularly the 2013 paper. Thank you for the links.

I think Bertrand Meyer was trying to solve actual problems that programmers face (which do imply co-variance in OO languages), instead of trying to solve theoretical "type system theory" problems. His choices were rational and fit the actual use cases well, (although I never liked Eiffel itself -- fortunately I haven't had to use it in over 20 years now).

Also, while co-variance does imply (for type safety) a mechanism "like a C++ dynamic cast" at some point in the process, that cost can be almost zero (with no latent per-invocation cost) if the types actually match, and can be nominal (one indirection or preamble) for type ambiguities -- and with that cost only being present for methods whose parameters and/or return values exhibit type ambiguities.

(I don't know if the Eiffel implementation was that efficient. Regardless, the implementation does not have to be inefficient.)

By cpurdy at Wed, 2019-01-09 14:42 | login or register to post comments

Hmm

I think Bertrand Meyer was trying to solve actual problems that programmers face (which do imply co-variance in OO languages), instead of trying to solve theoretical "type system theory" problems. His choices were rational and fit the actual use cases well, (although I never liked Eiffel itself -- fortunately I haven't had to use it in over 20 years now).

I got the impression that he was trying to stick to theoretical principles with the language and was not quick to duck tape over the variance problem in the name of practice. But he eventually decided that the extra theoretical tools he'd need to fix the problem were going to be too much extra complexity.

By Matt M at Fri, 2019-01-11 04:07 | login or register to post comments

You have piqued my curiosity!

But he eventually decided that the extra theoretical tools he'd need to fix the problem were going to be too much extra complexity.

Do you have any additional information on that?

By cpurdy at Fri, 2019-01-11 21:15 | login or register to post comments

I'm not sure where my

I'm not sure where my impressions originate. I've read two of his books but it's been quite while. I can find this c2 wiki which links to this paper on covariance by Meyer. I think I've read that paper at some point, too. Reading over it now, I think I may have mis-characterized his position, but it does show that he didn't take the matter lightly.

By Matt M at Sat, 2019-01-12 03:39 | login or register to post comments

One alternative to consider

One alternative to consider is to use co-variance for everything, and perform a run-time check to be sure that the run-time type tag matches when there are multiple operands. For example, if you have a user-defined "+" operator on a type T, returning T, then the signature of the corresponding operator for type T1 that is an extension of T would be:

op "+" (T1, T1) -> T1

If you then try to add two objects whose run-time type tag is not known statically, a check is made that they identify the same type, and that type's "+" operator is chosen. The only special case worth recognizing is probably the equality operator, where if the run-time type tags don't match you simply return False without invoking the type-specific equality operator. This allows each type-specific operator to have no concerns about type mismatches, and to only deal with the type of operands it was designed for.

By sttaft at Sun, 2019-02-10 18:33 | login or register to post comments