[TYPES] Types in distributed systems

[Andreas Rossberg]

On Sep 2, 2014, at 13:31 , Ionuț G. Stan <ionut.g.stan at gmail.com> wrote:
> Part of the same stream of questions I had initially was where would the Java Virtual Machine be situated in this picture. A single JVM process isn't distributed, and yet, one may still encounter similar situations to those that I imagined in original email, but due to classpath conflicts this time. I'm pretty confident now that the JVM can be classified as an open system.

Yes, indeed.

> Case in point. On the JVM, one may end up in a situation where two libraries I'm depending upon, depend in turn on the same third library, *but* different versions of it. My code will compile just fine, because transitive dependencies aren't verified statically. At runtime, though, only one of those two versions of the third library will win and one of the possible outcomes is the dreaded java.lang.NoSuchMethodException.
> 
> Although I cannot articulate it precisely, I feel there's a gap between, e.g., having a runtime check for out of bounds array indeces, on one hand, and missing method definitions at runtime on the other hand. As a library author, if I'm calling a function or method from an external module and my code compiles then I have a static *guarantee* that that method will be there at runtime, isn't it?
> 
> Am I missing something or is this not a useful difference to make in practice/theory?

Right, as others have observed in the past, Java effectively is an untyped language. Whatever its type system pretends to check is not a static guarantee of anything, at least not for object types. That is because there is no sound type checking when linking against a referenced class. In general, the classes you see at runtime time bear no relation to whatever you had imported at compile time (other than their syntactic name).

But this is a failure of Java and the JVM. It can be fixed, e.g. by doing a structural, link-time type check for every import edge. That is e.g. the approach we used in Alice ML, which is a version of SML extended with dynamic modules and a programmable “component manager", very much in the spirit of Java’s class loader, but without the soundness breakage (e.g. described in http://www.mpi-sws.org/~rossberg/papers/missing-link.pdf, if you apologise the self reference :) ).

/Andreas