[TYPES] Types in distributed systems

[Mark Sheldon]

I’m enjoying this discussion, so thank you for raising the issues!  The issues related to dynamic linking in the JVM really takes me back...

We ran into these problems of dynamic linking way back in the 1980s/90s when working on a language (FX) with first-class modules.  Modules in FX defined/implemented abstract types, and having them be first-class meant they were dynamically loaded, but we wanted static type checking.  A fun result is that such a language acts as its own linking language (or, I suppose you could say, there is no longer a need for separate linking language).  

Our solution was this:  We used a unique ID for each version of a module/library.  That ID could in principle be the source code for the library, a unique hash of that, etc.  We used a system with names and time stamps, which was ok in a non-distributed setting.  Compiled code retained the IDs of modules it was compiled against, and loading the modules involved checking that the library you’re loading matched the one used at compilation.  If you kept multiple versions of a module around, you could have different versions loaded and successfully manipulate instances of the different versions.  The static type checker would ensure that you could not send an instance module M version 1 to an operation expecting an instance of module M version 2:  the two modules would be considered mutually incompatible.  We had no notion of specifying anything like backward compatibility or induced subtype relationships, which is really something you want for distributed protocols, for example.

This is surely superseded by more recent work, some cited in this thread, but if you’re interested, we had a paper in the 1990 Lisp and Functional Programming Conference.  

It was our little version of DLL hell :-)

-Mark

Mark Sheldon
msheldon at cs.tufts.edu

On Sep 4, 2014, at 4:55 AM, Andreas Rossberg <rossberg at mpi-sws.org> wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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
>