This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Re: Proven immutable classes?

2 replies
rytz
Joined: 2008-07-01,
User offline. Last seen 45 weeks 5 days ago.

Hi Jonathan,

in the course of a semester project, Davide Galimberti (EPFL student) recently
implemented a prototype of the Javari [1] system as a Scala compiler plugin.

The system not only allows to check whether a class is immutable, it also allows
tracking immutable references (aliases) to potentially mutable objects. It guarantees
that no state modifications are performed through an immutable reference.

His report is attached, the source code is available on svn
http://lampsvn.epfl.ch/svn-repos/scala/compiler-plugins/immutability/trunk
http://lampsvn.epfl.ch/trac/scala/browser/compiler-plugins/immutability/trunk


Cheers: Lukas


[1] Matthew Tschantz, Michael Ernst. Javari: Adding Reference Immutability to Java


On Wed, Mar 10, 2010 at 02:53, jonathan mawson <umptious [at] gmail [dot] com> wrote:

I was going to ask something very like this - but not so much "Should Scala
have this?" as "Does Scala have this?" No one replied to the question below,
although to me it seems a very good one.

>>>>
http://old.nabble.com/Could-proved-immutable-classes-be-added-to-Scala--td14626792.html

Since Scala makes a point of allowing both the immutable/functional and
mutable/imperative styles of programming, it could benefit from a means
of saying formally whether a class is immutable or not. Of course, it
could be mentioned in ScalaDoc comments, and made sure by the
implementers, but I think something *formal* and (somewhat) *proved*
would be better. And could probably lead to some optimization
possibilities or better tools in the future.

For example, an annotation @immutable or trait Immutable that could be
added to types, objects of which are intended to be immutable. The
compiler would check that these classes meet certain conditions that
prove them immutable, otherwise raise an error.
Coming from imperative programming, most recently Java (and having had
very little to do with FP), I may be displaying my ignorance, but as far
as I know, the following should be enough to prove a Scala class
immutable (I'm sure many people here know better if this is wrong):
1) it doesn't extend any mutable classes (only extends those that were
already proved immutable)
2) it doesn't declare any variable members
3) it doesn't declare mutable constructor arguments
4) it doesn't declare mutable value members, maybe not even lazy values?
5) is final or it's subclasses must also be immutable
6) function types are not considered immutable
(optional 7) doesn't use any mutable classes in any way at all -- this
might not be required, I think, it probably depends on what level of
immutability is wanted)

Some side effects/notes:
* Any class that extends an immutable class must be immutable
* like a case class, equals and hashCode should be generated based on
constructor arguments (but if manually written, these methods would not
be checked for correctness of course)
* java.lang.String must be specially marked immutable somehow, also
possibly other classes that I'm missing

Would this be very hard to implement? Or does it even make sense?

Erkki
<<<<
--
View this message in context: http://old.nabble.com/Proven-immutable-classes--tp27844620p27844620.html
Sent from the Scala - Debate mailing list archive at Nabble.com.



Randall R Schulz
Joined: 2008-12-16,
User offline. Last seen 1 year 29 weeks ago.
Re: Proven immutable classes?

On Wednesday March 10 2010, Donna Malayeri wrote:
> The math/logic stuff is certainly all "discovered." The
> implementation came from a mysterious extra-terrestial black box in
> Lausanne.

Most likely something transported back in time as part of a desperate
attempt by physicists of the future to prevent the activation of the
LHC.

RRS

Naftoli Gugenheim
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
Re: Proven immutable classes?

Well, some people seem to think the world came into being by accident, so maybe someone really did guess the right sequence of numbers--the latter has a higher probability of happening statistically.
Only problem is, it breaks the premise of some software, like generating a random string and using it as a unique id, because the chances of generating the same string twice is less than that of a meteorite falling on you. Or was it a comet? This could be relevant to Lift -- they use random strings for unique ids and they support comets.

-------------------------------------
Dimitris Andreou wrote:

As any piece of software, scala at the end of the day is nothing more than a
set of bits, i.e. a number (which also happens to have some useful
properties). Now, can anybody claim the "invention" of a number? :)
Additionally, if you were to be lucky enough, and made a (very!) wild guess
and ended up with that very number, well, you would have been the
inventor/discoverer of scala now!

2010/3/10 christopher marshall

> This leaves me confused about one thing: are we now saying that Scala was
> "discovered", not invented? Those EPFL frauds!
>
> ------------------------------
> Date: Wed, 10 Mar 2010 14:17:30 +0000
> Subject: Re: [scala-debate] Proven immutable classes?
> From: kev [dot] lee [dot] wright [at] googlemail [dot] com
>
>
> Nobody back then knew "what's left" for physics, so would it be wise to
> make the same mistake in thinking about Scala?
>
>
>
> ------------------------------
> We want to hear all your funny, exciting and crazy Hotmail stories. Tell
> us now
>

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland