[isabelle-dev] ADTs in Scala

[Alexander Krauss]

On 04/14/2012 07:43 PM, Makarius wrote:
> The starting point of the whole affair was the problem of having a
> public class where the default constructor (or any further ones) are
> private.

>
> I did not know how to do it, until some Java expert talk about the
> potential future of Java (after 1.7 or 1.8) explained that default
> constructors were always as public as the class they belong to. This
> solved my problem, because I knew what to google for concerning Scala,
> namely "private constructor".
>
> Accordingly the solution in Scala is:
>
> final class Graph[Key, A] private(rep: SortedMap[Key, (A,
> (SortedSet[Key], SortedSet[Key]))])
> ^^^^^^^

Your conversation with the Java expert must have involved some 
misunderstanding:

In Java:

public final class Graph {

   private final SortedMap<...> rep;

   // private constructor:

   private Graph(SortedMap<...> rep) {
     this.rep = rep;
   }

   // public static "factory methods"

   public static Graph empty() {


   }

   ...
}


Note that the so-called "default constructor" is only added when no 
constructor is defined explicitly. So the above is fine, modulo the 
usual Java verbosity.

For good contemporary Java coding practices, Joshua Bloch is the reference:
http://www.amazon.com/Effective-Java-Edition-Joshua-Bloch/dp/0321356683/

Alex