[isabelle-dev] ADTs in Scala

[Makarius]

On Mon, 16 Apr 2012, Holger Gast wrote:

> b) Coding conventions and usual practice (my addition to the above):
>   It is customary to make constructors, and not some auxiliary
>   static methods, responsible for proper initialization.

But this is exactly what did not work out smoothly.  The task is to make 
an implementation of *immutable* datastructures.  So you cannot just 
construct a new (empty) Graph and then invoke methods to update its state. 
You need to construct new graph objects from old ones in a manner that 
retains the intended semantics.

See 
http://isabelle.in.tum.de/repos/isabelle/file/f4348634595b/src/Pure/General/graph.scala 
for the concrete implementation we are speaking about.  Maybe you want to 
make a standard Java version from it -- with immutable objects, not 
mutable ones.


"Immutable object" might sound like an oxymoron for OO according to 1995, 
but it is commonplace in some leading edge communities.  Immutability is 
also the standard way in Isabelle/Scala (and Isabelle/ML) to get clean 
semantics and good performance in a parallel setting.

BTW, this thread emerged from another one about the JUNG framework, where 
graphs are mutable according to some old standard patterns.  This meant 
one had to clone the whole thing occasionally in the usual awkward way. 
The new graph.scala avoids all this extra overhead, and also the 
dependency of the huge JUNG framework.


 	Makarius