[isabelle-dev] ADTs in Scala

[Makarius]

On Sat, 14 Apr 2012, Lars Hupel wrote:

>> 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 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]))])
                             ^^^^^^^

This makes the main constructor private, as required for the idea of 
"abstract data type".  (I hope the above is waterproof -- there can be 
always semantic surprises on this platform.)


How would one do this in Java?  Via some auxiliary classes and extra 
visibility indications?


 	Makarius