[isabelle-dev] ADTs in Scala

[Tobias Nipkow]

May I remind the participants of this thread that this is the Isabelle
development mailing list, not a discussion forum on OO techniques in general.

Thanks
Tobias

Am 16/04/2012 16:57, schrieb 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
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev