[e-lang] Comments requested on paper: functional purity in Joe-E

[David Wagner]

Toby Murray writes:
>"In particular, there cannot be any cycles in immutable data
>structures." I don't get this.. What about
>
>public class Bar implements Immutable{
>   private Foo _foo;
>   public Bar(Foo foo){
>      _foo = foo;
>   }
>}
>public class Foo implements Immutable{
>   private Bar _bar;
>   public Foo(){
>      _bar = new Bar(this);
>   }
>}
>
>Would Foo not be considered Immutable?

Great example.  No, Foo doesn't qualify as an Immutable class, because
it violates some of Joe-E's rules.  Let me try to explain.

First, you'd need to add a "final" keyword to all of the fields.
The Joe-E verifier needs to know that you cannot change the value of the
fields once they have been initialized, and it does that by requiring
you to use the "final" keyword.

Second, the Joe-E verifier should flag an error in the Foo() constructor,
because the call "new Bar(this)" allows the this-pointer to escape.
We must prohibit that, for reasons that may seem a bit crazy at first.

The crazy reason is that, in Java, the "final" keyword does not actually
make a field final (i.e., doesn't make the field a constant throughout the
lifetime of the object).  Huh?  Yes, that's right.  The "final" keyword
does ensure that a field may be assigned to only once.  However Java
allows you to read the value of a field that has not yet been assigned
to, in which case the field has its default value (0, null, or false,
depending upon its type).  So if someone reads the value of this._bar
before it is assigned, and then reads it after this._bar has been
assigned, they will see two different values -- in violation of what
we'd expect from an immutable object.

You might not be familiar with this oddity of the Java language, because
Java makes a best-effort (but imperfect) attempt to prevent this kind
of unexpected behavior.  In particular, Java has something called the
"definite assignment" rules which are intended to ensure that a final
field is assigned at least once and at most once.

Unfortunately, the definite assignment rules have a hole: Java only does
intraprocedural analysis (inside the constructor), and Java does not
try to prevent other methods from reading a field that has not yet been
assigned.  The bad case can only happen if you allow the this-pointer
to escape from the constructor, because then other methods might be
able to get a reference to an incompletely-initialized instance (i.e.,
one where the constructor has not yet finished running) of the class.

So, to fix up the hole in Java's definite assignment rules, Joe-E
introduces restrictions which suffice to ensure that the this-pointer
cannot escape from the constructor.  As a result, if you run the Joe-E
verifier on the above example, I expect it to complain about the body
of the Foo() constructor.  (Give it a try and see if I've predicted
correctly!)

As a result, I believe it is correct that one cannot create cyclic
immutable data structures in Joe-E -- which is a shame.

We didn't really want to go into this in this paper, because we felt the
mechanism for verifying Immutability is a bit out of scope.  We plan
to write another paper focusing on the overlay type system and on the
mechanisms we use for enforcing Immutable types, including the issues
with the "final" keyword and some other peculiarities we ran across.