Re: [isabelle-dev] ADTs in Scala

2012-04-16 Thread Holger Gast
I usually make jokes at a longer historical range. [...] Anyway, this thread is diverging. I merely wanted to express my relief that I can now work in the classic ADT style from the 1970/80-ies almost unencumbered by ooddities in Isabelle/Scala. Sorry, I fail to see the joke. If you ask

Re: [isabelle-dev] ADTs in Scala

2012-04-16 Thread 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*

Re: [isabelle-dev] ADTs in Scala

2012-04-15 Thread Holger Gast
On 04/14/2012 03:09 PM, Makarius wrote: On Sat, 14 Apr 2012, Lars Hupel wrote: The main thing is the private in this odd position, which is Odersky's way to make the constructor private, but the keep the type itself public. This detail seems to have been forgotten in Java -- in fact in a

Re: [isabelle-dev] ADTs in Scala

2012-04-15 Thread Makarius
On Sun, 15 Apr 2012, Holger Gast wrote: In fact, the pattern you used is quite common amongst Java developers, they just call it Factory Pattern. I've heard of this recent addition to the OO vocabulary to fix some early conceptual problems of the approach. That is object Graph part only.

Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Lars Hupel
object Graph { // public operations to create ADT instances } final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) { // implementation with access to rep } The main thing is the private in this odd position, which is

Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Makarius
On Sat, 14 Apr 2012, Lars Hupel wrote: The main thing is the private in this odd position, which is Odersky's way to make the constructor private, but the keep the type itself public. This detail seems to have been forgotten in Java -- in fact in a recent talk some Java guru admitted that --

Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Lars Hupel
I've heard of this recent addition to the OO vocabulary to fix some early conceptual problems of the approach. That is object Graph part only. How would a Java person solve the private constructor problem? Could you explain a bit more? -- Java has private constructors. The source file