Re: Comments requested on paper: functional purity in Joe-E

On Wed, 2008-06-04 at 10:10 -0700, David Wagner wrote:
> Toby Murray writes:
> >"In particular, there cannot be any cycles in immutable data
> >structures." I don't get this.. 

>  Let me try to explain.

> The crazy reason is that, in Java, the "final" keyword does not actually
> make a field final.
> 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.  
> 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, I believe it is correct that one cannot create cyclic
> immutable data structures in Joe-E -- which is a shame.

Thanks for the lucid explanation. Makes perfect sense now and I agree
with the assertion in the paper.


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

Fair enough indeed. This paper's focus is elsewhere I understand.

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

Cool. Looking forward to it.

Thanks again

Toby