[isabelle-dev] ADTs in Scala

[Makarius]

On Sat, 14 Apr 2012, Alexander Krauss wrote:

>> Accordingly the solution in Scala is:
>> 
>> final class Graph[Key, A] private(rep: SortedMap[Key, (A,
>> (SortedSet[Key], SortedSet[Key]))])
>> ^^^^^^^
>
> 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.

OK, this means that Odersky did not introduce another workaround for a 
Java problem, but merely provide his own short notion for what was there 
already.


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

I did not mean to engage in Java.  For me it is just the accidental 
implementation language of some JVM-based frameworks that are used in 
Isabelle/Scala.


 	Makarius