1
$\begingroup$

In any Object-Oriented type system the type relation of two objects A and B can be characterized in exactly one of the following ways:

  • A has the same type as B
  • A is a subtype of B
  • B is a subtype of A
  • A and B are not (directly) related.

My goal is to define an ordering relation which I can then use to demonstrate covariance and contravariance. The canonical ordering relation used for this in literature is a <: b, which is defined as "a is a subtype of b".

Since my math course at university (1st semester CS) has only covered partial orders so far, I tried starting with a simple partial order:

We can establish a well defined order relation between two types as "X is a subtype of or of the same type as Y", written as X <:= Y because it fullfils the three neccessary properties

  • Reflexitivity: For all types T, T<:= T.
  • Antisymmetry: For all types T and U, T <:= U and U <:= T implies U = T
  • Transitivity: For all types S, T and U S <:= U and U <:= T implies S <:= U

Now my problem is that I want to use this to show that covariant means (from wikipedia):

a type operation is called covariant if it preserves the ordering, ≤, of types, which orders types from more specific to more generic;

I guess I'm in conflict with the definition if I substituted <: with my made up <:= relation here. However, this is just a gut feeling. So in order to arrive at <:, I'd need to make my partial ordering <:= a strict total ordering (if I understood correctly).

From a logical perspective this seems simple, however I struggle with the mathematically correct way of formulating this. Wikipedia seems to suggest that it should be possible:

Contrast this [a total order] with a partial order, which has a weaker form of the third condition (it only requires reflexivity, not totality).

...

For each (non-strict) total order ≤ there is an associated asymmetric (hence irreflexive) relation <, called a strict total order

It seems I'm almost there, however this is completely new terrain for me and I'd like to how this could be done actually.

$\endgroup$

closed as off topic by Neel Krishnaswami, Dave Clarke, Suresh Venkat Jan 28 '11 at 18:59

Questions on Theoretical Computer Science Stack Exchange are expected to relate to research-level theoretical computer science within the scope defined by the community. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about reopening questions here. If this question can be reworded to fit the rules in the help center, please edit the question.

  • $\begingroup$ btw, this is my first post on cstheory, so please feel free to correct tags if they are incorrect. $\endgroup$ – Johannes Rudolph Jan 27 '11 at 23:25
  • $\begingroup$ what is the type operation that you wish to show is covariant though $\endgroup$ – Suresh Venkat Jan 28 '11 at 0:01
  • 1
    $\begingroup$ I'd appreciate if you showed some links to the wikipedia definitions you're working from. I think the subtype relation already gives what you want. a <: a is always true, and my understanding is that subtyping is always a partial order. You basically want to end up with a lattice of types: en.wikipedia.org/wiki/Lattice_(order) $\endgroup$ – sclv Jan 28 '11 at 0:51
  • 4
    $\begingroup$ This is not a research-level question. Variance is not a property of types, but of type operators. Given a lattice of types partially ordered by subtyping, a type operator is an endofunction on this lattice. Covariance means the operator is monotone, and contravariance means it is antitone. $\endgroup$ – Neel Krishnaswami Jan 28 '11 at 3:30
  • 1
    $\begingroup$ @Johannes Rudolph: as a first semester CS student, you have the luck of having many wonderful discoveries ahead of you, and it is great to see you exploring these ideas on your own. If you want to jump ahead and start exploring type systems, I suggest that you look at the book: Types and Programming Languages by Benjamin Pierce or the manuscript by Bob Harper: cs.cmu.edu/~rwh/plbook/book.pdf. These might be a little tough going at first, but they will open you to a world of delight. $\endgroup$ – Dave Clarke Jan 29 '11 at 10:22