[PRL] the "success" of types

[Felix S Klock II]

On May 20, 2006, at 4:37 PM, William D Clinger wrote:

> John Clements wrote:
>> That is, to the best of my knowledge I can't write an invariant that
>> states:
>>
>> Right now, x and y are both lists of some type T (though at other
>> times they might not be of the same type).
>>
>> ... whereas I _can_ write
>>
>> This procedure accepts two lists that must both contain the same  
>> type T.
>
> import java.util.*;
>
> public class Foo {
>
>     public static int counterexample (List x, List y) {
>         List<Integer> xint = (List<Integer>) x;
>         List<Integer> yint = (List<Integer>) y;
>         return (xint.size() + yint.size())
>             * (xint.get(0).intValue() + yint.get(0).intValue());
>     }
>
>     public static void main (String[] args) {
>         List x = new ArrayList();
>         List y = new ArrayList();
>         x.add(11);
>         y.add(12);
>         System.out.println (counterexample (x, y));
>     }
> }
>
> ****************************************************************
>
> % javac Foo.java
> Note: Foo.java uses unchecked or unsafe operations.
> Note: Recompile with -Xlint:unchecked for details.
> % java Foo
> 46

I'm sorry, what was this point of this example?

John said that you can't write down certain time dependent invariants  
of practical interest.  I inferred that he wanted this invariant to  
be automatically checked (statically, I assume, though some may be  
happy with a dynamic check, as long as it happens at a sensible  
place).  There may be some requirement on the programmer to provide  
some sort of proof that the invariant is not violated in whatever  
John is envisioning, I don't know.

Will responded with some source code, where an example of an  
invariant John would want to express was encoded as part of the type  
casts at points within the body of the counterexample() method.  The  
compiler spit out a warning saying that it couldn't actually prove  
that the invariant holds (so we didn't get our wish of an automatic  
static check that the invariant is maintained).  I don't think this  
compile-time warning is what John was asking for.

Something that Will omitted from his example was an attempt to call  
counterexample with a List that holds a non Integer object in slot  
0.  This would be an important example to include, because it would  
illustrate where the violation of the invariant is detected by the  
Java runtime.  My hypothesis is that the error will be signaled at  
the invocation of the .intValue() method (but I have not checked this  
hypothesis; its just based on my knowledge of type-erasure).  So if  
this is true, then we would find that stating John's invariant didn't  
actually buy us anything; it wasn't checked at the point of the cast  
expression, so what was the point writing that invariant down?

So, again, my question: why was this a counterexample to John's claim  
that you can't express what he wants in Java?  (I believe C#, on the  
other hand, carries the type instantiation information around, so it  
should be possible for it to detect the error during the evaluation  
of the cast expressions.  But that wasn't what John was pointing out.)

-Felix