[isabelle-dev] ADTs in Scala

Holger Gast gast at informatik.uni-tuebingen.de
Mon Apr 16 15:00:21 CEST 2012

>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 explicitly
"How would a Java person solve this problem?" there are two answers:

a) Technical rules about constructors (Alex's answer):
   1) Constructors can have any desired visibility, including private,
      protected, and default (Guy Steele certainly knows how to design
      orthogonal language features; all a necessary and useful at times)
   2) default constructors are generated only if no explicit constructers
      are present.

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.


More information about the isabelle-dev mailing list