[isabelle-dev] ADTs in Scala

[Holger Gast]

> 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.

The the aspect of being immutable or mutable is, of course, orthogonal of the 
question of proper initialization: in either case, the construction in the
end must leave the object in a consistent state such that it can be used 
further. Whether one uses the object thus created to

a) modify the object's data as done in most current OO code
b) create new objects by calling constructors/static methods
c) create new objects by methods that produce new results

is quite irrelevant here.

In the current example of graphs, the issue of "consistency"
may not be so obvious, because it has a single field that by itself
is, of course, trivially consistent.

--
Holger