[isabelle-dev] ADTs in Scala

Lars Hupel hupel at in.tum.de
Sat Apr 14 15:51:40 CEST 2012

> 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 source file 'graph.scala' looks fine the way it is now (except that
you don't have to pass the implicit parameters around explicitly). Note
that Scala allows secondary constructors, which would allow rewriting
`empty` as

def this(implicit ord: Ordering[Key]) = this(SortedMap.empty)

However, I don't see that very often in practice. The advantage of
`Graph.empty` is that it clearly communicates what this "factory" does.

More information about the isabelle-dev mailing list