[isabelle-dev] ADTs in Scala

Makarius makarius at sketis.net
Sun Apr 15 21:31:47 CEST 2012

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.
> Just for a reference: factories have been discussed in the seminal book 
> on patterns, Gamma et al. "Design Patterns: Elements of Reusable 
> Object-Oriented Software", in 1995. (There are two variants here: 
> abstract factories and factory methods, but this is only a detail.)

I usually make jokes at a longer historical range.  The classic OO times 
are about 10 years earlier than the Gang-of-Four stuff.  When I got to 
that again around 2007, I was surprised what is now called 
"object-oriented" compared to 15 years before.

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.

The explanation by Alex clarified things especially well: Java does allow 
all constructors to be private for a public class, but the way Odersky 
writes classes requires an additional syntactic device to indicate the 
visibility of the the main constructor.

Concerning style: Scala admits many styles, which is both an advantage and 
disadvantage, also due to general language complexity.  For example, the 
scalaz community writes Scala like Haskell, which might look a bit odd to 
many. The style of Isabelle/Scala is that of Isabelle, i.e. the best from 
many decades of Isbelle/ML transferred to Scala in a reasonable way.


More information about the isabelle-dev mailing list