Re: Typing in Java

   Date: Fri, 19 Jun 1998 10:27:41 +0100
   From: chorn@lionet-technologies.com (Christian Horn)

   [------- The Types Forum ------ http://www.cs.indiana.edu/types -------]

   The problem mentioned has nothing todo with the
   conditional expression and not with Java, but with the way reduction
   for typed languages has to be formulated with casting
   of the actual parameter types to the formal parameter types.

   >   m(a1...an)  -->  r[((T1)a1)/x1...((Tn)an)/xn]

Indeed the issue here isnt that "Subject reduction" is violated
(it is preserved for "exact types"), but that, as Kim just
remarked, the conditional violates the "OO polymorphism property":

  If an expression e is soundly typed under the assumption that
  variables X1,...,Xn have type T1,...,Tn respectively, then it
  is soundly typed under the assumption that X1,..., Xn have
  types T1', ..., Tn' respectively, where each Ti' is a subtype of Ti.