Re: [isabelle-dev] ADTs in Scala

2012-04-16 Thread Holger Gast
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.

--
Holger
   


___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] ADTs in Scala

2012-04-16 Thread Holger Gast
 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.
But this is exactly what did not work out smoothly.  The task is to make 
an implementation of *immutable* datastructures.  So you cannot just 
construct a new (empty) Graph and then invoke methods to update its state. 
You need to construct new graph objects from old ones in a manner that 
retains the intended semantics.

The the aspect of being immutable or mutable is, of course, orthogonal of the 
question of proper initialization: in either case, the construction in the
end must leave the object in a consistent state such that it can be used 
further. Whether one uses the object thus created to

a) modify the object's data as done in most current OO code
b) create new objects by calling constructors/static methods
c) create new objects by methods that produce new results

is quite irrelevant here.

In the current example of graphs, the issue of consistency
may not be so obvious, because it has a single field that by itself
is, of course, trivially consistent.

--
Holger
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] ADTs in Scala

2012-04-15 Thread Holger Gast
On 04/14/2012 03:09 PM, Makarius wrote:
 On Sat, 14 Apr 2012, Lars Hupel wrote:
 
 The main thing is the private in this odd position, which is Odersky's
 way to make the constructor private, but the keep the type itself
 public. This detail seems to have been forgotten in Java -- in fact in a
 recent talk some Java guru admitted that -- which was also my starting
 point to google for private constructor to find the above solution.

 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.)

 How would a Java person solve the private constructor problem?
One would simply define the public default constructor
(or more precisely: zero-argument constructor) to provide a fully initialized
empty graph by setting the fields appropriately. This approach does not
destroy the properties of abstract data types, since the invariants
remain under the class's control and clients cannot break the abstraction.
In effect, the solution merely reflects the (sensible) convention that the
default content of data structures is empty. The Java standard
library uses this throughout: writing new HashMap() yields an empty
HashMap, just as expected.

As Lars has pointed out, it is a common coding pattern to complement
constructors by static construction methods to allow the method
names to designate clearly the expected initial content. It is
usually considered a matter of style, and the number of
constructors and their arguments, which formulation is preferable.

Actually, even with such factory methods, it is usually left to the
constructors to do the proper initialization according to the
desired invariants etc. The static methods merely pass on parameters
and thus select the right constructor.

I hope this somewhat historical review helps in the discussion of
coding idioms  practices,

Best wishes,

 Holger
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] ADTs in Scala

2012-04-15 Thread Makarius

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.



Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Lars Hupel
   object Graph
   {
 // public operations to create ADT instances
   }
 
   final class Graph[Key, A] private(rep: SortedMap[Key, (A,
 (SortedSet[Key], SortedSet[Key]))])
   {
 // implementation with access to rep
   }
 
 The main thing is the private in this odd position, which is Odersky's
 way to make the constructor private, but the keep the type itself
 public. This detail seems to have been forgotten in Java -- in fact in a
 recent talk some Java guru admitted that -- which was also my starting
 point to google for private constructor to find the above solution.

In fact, the pattern you used is quite common amongst Java developers,
they just call it Factory Pattern.

 Next inappropriate question for Scala: How to avoid the ubiquitious NPE
 problem of the JVM?

This question is not inappropriate at all. There is no single strategy
to avoid NPEs, but usually, Scala programs make extensive use of
`Option` to wrap anything that comes from a Java library to make sure
that there are no `null`s involved. Scala's API has a nice `Option`
factory for that: write `Option(value)`, and get `None` for `null` and
`Some(x)` for `x != null`. Obviously, computations then have to be
rewritten in applicative or monadic style. For the latter, Scala has
sugar in form of for comprehensions.

On a related note, there is also Scala library support to avoid the
general exception problem on the JVM. (see
http://www.scala-lang.org/api/current/index.html#scala.util.control.Exception$)

-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Makarius

On Sat, 14 Apr 2012, Lars Hupel wrote:


The main thing is the private in this odd position, which is Odersky's
way to make the constructor private, but the keep the type itself
public. This detail seems to have been forgotten in Java -- in fact in a
recent talk some Java guru admitted that -- which was also my starting
point to google for private constructor to find the above solution.


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.


How would a Java person solve the private constructor problem?


Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] ADTs in Scala

2012-04-14 Thread Lars Hupel
 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.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev