<p>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:</p>

<ul>
<li>A has the same type as B</li>
<li>A is a subtype of B</li>
<li>B is a subtype of A</li>
<li>A and B are not (directly) related.</li>
</ul>

<p>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 <code>a &lt;: b</code>, which is defined as "a is a subtype of b".</p>

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

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

<ul>
<li>Reflexitivity: <code>For all types T, T&lt;:= T.</code></li>
<li>Antisymmetry: <code>For all types T and U, T &lt;:= U and U &lt;:= T implies U = T</code></li>
<li>Transitivity: <code>For all types S, T and U S &lt;:= U and U &lt;:= T implies S &lt;:= U</code></li>
</ul>

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

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

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

<p>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:</p>

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

<p>...</p>

<blockquote>
  <p>For each (non-strict) total order ≤
  there is an associated asymmetric
  (hence irreflexive) relation &lt;, called
  a strict total order</p>
</blockquote>

<p>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.</p>

CC BY-SA 2.5
2011-01-27T23:25:12.573Z
btw, this is my first post on cstheory, so please feel free to correct tags if they are incorrect.
Johannes Rudolph
CC BY-SA 2.5
2011-01-28T00:01:55.463Z
what is the type operation that you wish to show is covariant though
Suresh Venkat
CC BY-SA 2.5
2011-01-28T00:51:49.643Z
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: http://en.wikipedia.org/wiki/Lattice_(order)
sclv
CC BY-SA 2.5
2011-01-28T01:13:12.813Z
I think that your `<:=` is the same as the usual `<:`.
Tsuyoshi Ito
CC BY-SA 2.5
2011-01-28T03:30:42.860Z
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.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-28T10:46:51.487Z
I agree with Neel. Have you read books on (object-oriented) types systems, such as those by Pierce, Cardelli & Abadi, Castanga, Bruce?
Dave Clarke
CC BY-SA 2.5
2011-01-28T15:55:37.843Z
@Neel: Yes, this is not a research-level question, as I mentioned before I'm a 1st semester CS student and the mathemtaical definition of co- and contravariance was simply intriguing me and I wanted to investiage what's behind it. I wasn't aware this is a research-level only SE, this question should probably be moved to math.se then.
Johannes Rudolph
CC BY-SA 2.5
2011-01-28T16:21:34.353Z
@sclv: Thanks for pointing this out, I think that 'a <: a' is always true was the missing piece for me, hence a strict total order relation seems not to be required for defining co and contravariance. The reason I was asking is that if a partial order is sufficient, we could call an identity cast (int -> int) a covariant operation (because it preserves the ordering of types)?
Johannes Rudolph
CC BY-SA 2.5
2011-01-29T10:22:53.910Z
@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: http://www.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.
Dave Clarke
CC BY-SA 2.5
2011-01-29T16:29:09.617Z
@Dave: Thanks for that hint. I'll try to look into it as soon as I find the time for it. Thank you very much!
Johannes Rudolph
<type-theory><partial-order><total-ordering>
Well Defined Ordering Relations in Object Oriented Type Systems
Johannes Rudolph
# Well Defined Ordering Relations in Object Oriented Type Systems

(Asked by: username_0 on 2011-01-27)

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.

**Tags:** type-theory, partial-order, total-ordering
> **Comments:**
> **username_0**: btw, this is my first post on cstheory, so please feel free to correct tags if they are incorrect.  
> **username_1**: what is the type operation that you wish to show is covariant though  
> **username_2**: 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: http://en.wikipedia.org/wiki/Lattice_(order)  
> **username_3**: I think that your `<:=` is the same as the usual `<:`.  
> **username_4**: 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.  
> **username_5**: I agree with Neel. Have you read books on (object-oriented) types systems, such as those by Pierce, Cardelli & Abadi, Castanga, Bruce?  
> **username_0**: @Neel: Yes, this is not a research-level question, as I mentioned before I'm a 1st semester CS student and the mathemtaical definition of co- and contravariance was simply intriguing me and I wanted to investiage what's behind it. I wasn't aware this is a research-level only SE, this question should probably be moved to math.se then.  
> **username_0**: @sclv: Thanks for pointing this out, I think that 'a <: a' is always true was the missing piece for me, hence a strict total order relation seems not to be required for defining co and contravariance. The reason I was asking is that if a partial order is sufficient, we could call an identity cast (int -> int) a covariant operation (because it preserves the ordering of types)?  
> **username_5**: @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: http://www.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.  
> **username_0**: @Dave: Thanks for that hint. I'll try to look into it as soon as I find the time for it. Thank you very much!  

---

## 0 answers

