About rule (T-SCast) in FJ and downcasting in Java

In [IPW] the authors describe the type system of Java, but extends it with the rule (T-SCast). Why?

Well. The type system of Java (essentially the type system of FJ without rule (T-SCast) ) is type-unsafe. In fact it cannot prevent us to write a program producing the following type error, as showed in [IPW]:
If we define the following classes:

class A extends Object {
    A() {super(); }
 
}

class B extends Object {
    B() {super(); }
 
}

then the evaluation of the following well-typed expression results in a run-time error of the sort a type system should actually prevent.

(A)(Object)new B()

Question 1: How can we guarantee a well-typed Java program not to produce this sort of type errors?

Question 2: Are there other run-time errors which can occur during the execution of well-typed Java programs?

These questions are answered in [IPW]. Let us briefly sketch how.
An expression is called safe if it is well-typed and rules (T-DCast) and (T-SCast) are not used. In the theorems 2.4.2 and 2.4.4 it is proved that no safe expression can contain subexpressions of the following form

• (C)New C₀(e)   with C₀ not a subtype of C.
• New C₀(e).f   with f not among the fields of class C₀.
• New C₀(e).m(d)   with m not among the methods of the class C₀ or the number of arguments d different from the number of aruments required by m.

This means that the evaluation of a safe expression is not blocked because of
(1) a wrong cast or
(2) a wrong field selection (nonexistent-field) or
(3) a wrong method invocation (method-not-understood).
So, in order to show that during the evaluation of a safe expression no run-time error (1), (2) or (3) can occur, it is enough to prove that reduction preserves safeness of expressions (Th.2.4.3). In order to prove Th.2.4.3 it is necessary to prove the Subject Reduction property (Th.2.4.1).
But the subject reduction property cannot be proved for the type system of Java, and in particular for the type system of FJ without rule (T-SCast) !!
In fact the expression (A)(Object)new B() is well-typed in Java, but the expression obtained after just one step of evaluation, that is (A)new B(), is not well-typed.
Any way out?
Yes. We extend the type system of FJ with rule (T-SCast) and this allows the Subject Reduction property to hold. (Theorem 2.4.1 of [IPW]).

So now we know that well-typed Java programs are potentially type-unsafe, i.e. they can get stuck, but the cause of that lies only in the use of downcasts. Programs that do not use downcasts at all are type-safe, i.e. no error (1), (2) or (3) can ever occur during the execution.

A small doubt still remains: the type system of FJ is not precisely the one of Java: it contains rule (T-SCast)...
We have to consider however that if we take a program well-typed in the type system without (T-SCast), such a program is also well-typed in the type system that uses (T-SCast)... so the above properties holds also for it. In fact, for well-typed programs in Java, rule (T-SCast) is needed only to type some expressions obtained during their evaluation.

Question 3: If the downcast is dangerous, why does Java use it?

Well, for instance in order to overcome some problems due to the fact that in overridden methods the type of the domain and codomain of a method cannot change. Here is an example of such a problem:

Let us assume to have a class Animal with the following binary method

public boolean compatible (Animal p) {

....

}

This method checks whether two animals can stay together

Now let us assume we have also a class Dog wich is a subclass of Animal and we wish to redefine the method compatible in order that, in case two dogs are compatible, they also bark.
The redefined method, by the Java typing rules, cannot take a Dog as argument, but an Animal. So if in the body of the redefined method we write p.bark() we get a type error detected statically, since p is considered to belong to the class Animal, where no method bark is present.

So, we are forced to use the downcast in the redefined method:

public boolean compatible (Animal p) {

.... (Dog)p.bark() ....

}

The problem now is that the type system will not prevent us to take a Dog fido and a Toucan tuky and write somewhere

 fido.compatible(tuky)

Now the method compatible will try to make tuky bark!!!

Of course we could use instanceOf, but doing this would mean that we are doing a work that should be done by the type system.

So, downcasting helps us to solve a problem, but produces another problem....

Note: The introduction of Generics in Java makes unnecessary the use of dangerous type casts. Generics in fact make unnecessary the downcasts from Object. Type safety can still be broken, but programmers have now the possibility not to do that.
Note: From version 1.5 on, Java allows to have covariant return types for redefined methods.
(Thanks to Sara Capecchi)