[isabelle-dev] ADTs in Scala
makarius at sketis.net
Mon Apr 16 16:15:03 CEST 2012
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.
for the concrete implementation we are speaking about. Maybe you want to
make a standard Java version from it -- with immutable objects, not
"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.
More information about the isabelle-dev