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
For all types T, T<:= T.
For all types T and U, T <:= U and U <:= T implies U = T
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.