[Prev][Next][Index][Thread]
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.