[e-lang] e-lang Digest, Vol 52, Issue 4

[Adrian Mettler]

Mike Samuel wrote:
> 
> In 2.6 you talk about assertions and the guarantee of purity.  I'm
> unclear on how this achieves that goal.  In a pure function, I assume
> all my assertions need to be pure.  How can I assert post-conditions
> on my output which, if I understand the definition, may not be
> immutable.
> 
The purpose of section 2 is primarily to motivate scenarios in which 
purity may be useful; while it is often the case that careful design
lets one use Joe-E to achieve purity in such scenarios "for free," some 
cases may be harder to prove pure than others and thus require more 
sophisticated analysis than what one can get from looking at signature 
of a Joe-E method.

We argue that purity is a useful property of assertions in general, as 
it allows one to know that they are deterministic and side-effect-free 
(and thus do not break the program when enabled).  In other words, 
verifiably pure assertions would be nice to have anywhere in one's code, 
not just in pure methods.  Unfortunately, we don't yet follow our own 
advice: the current Joe-E implementation does not require assertions to 
be pure, which means that the determinism guarantee for Joe-E code is 
parameterized on whether assertions are enabled (the same way as it 
depends on which version of the Java library is used).

On the other hand, you are right that some assertions are not easily 
made verifiably pure with our approach, as it is fairly restrictive on 
what one can do in the assertion condition.  One can always make the 
assertion pure by performing the not-verifiably-pure parts of the 
assertion check ahead of time, but this means that they won't be 
conditioned on whether or not assertions are enabled, reducing the 
performance benefit of disabling the assertions.
(e.g. change something like
assert mutableObject.getProperty() == EXPECTED_VALUE;
to
int temp = mutableObject.getProperty();
assert (temp == EXPECTED_VALUE);
)

Also, we would want to use a slightly different rule for determining the 
purity of an *expression* as occurs in an assert statement than for a 
method.  For example, the expression array[0] == 4 is clearly pure even 
though the entire condition could not be replaced with a single pure 
method call as a method that takes the array as an argument would not 
qualify as pure using our rules.  We don't actually apply our tool to 
showing that assertions are pure (we're focusing more on security 
applications) but the hypothetical "lint-like tool" we suggest would 
have to handle pure expressions like this.  The rule I had in mind was:
   the condition of the assert statement can read any field of any
   object, immutable or not, but can't use the assignment operators
   (= and +=) and can only call pure methods.
For Java, it is also necessary to wrap the assert statement in a wrapper 
that catches all exceptions and throws AssertError if any is 
encountered; otherwise enabling assertions could change behavior without 
failing the assertion if the assertion condition throws an exception. 
This complexity was another reason why we just stuck to explaining why 
purity is useful for assertions in the abstract rather than going into 
detail about how it could be achieved for Java using Joe-E.

> If I'd like to attach pre-conditions and post-conditions to my mutable
> class's methods, and know that they don't affect the behavior of the
> class, I can't since a pure function can't accept my mutable class as
> input.
>
Again, the conditions are expressions rather than method calls.  For 
some cases, this may be enough to make the conditions pure (e.g. if they 
depend on the values of primitive fields in the mutable class). 
Otherwise, you may need a more sophisticated analysis to ensure purity. 
  Like with assertions that require the calling of non-pure methods, one 
could introduce local variables that are computed even when the 
conditions aren't being verified at least for postconditions.  For 
preconditions, you might need a more sophisticated purity checker than 
you can get "for free" by using Joe-E.

> 
> In 4, you define "observationally functionally pure," and in 7.3.2 you
> talk about using an output Monad to collect debugging trace.  A
> library designer should not have to present a more complicated API to
> clients just so she can debug her system.
> 
> Does that definition of "observationally functional" admit a logging
> function that is a noop as far as Joe-E is concerned, but, combined
> with a java loader that bends the rules, might allow logging as
> described below.
> 
>   (1) A static Logger with a single declared public method void
>       log(String) {} doesn't prevent Joe-E code from being pure since
>       it appears just to be a dead drop.
>   (2) A test framework runs all unittests as normal with Logger
>       discarding its argument.  The JIT compiler probably inlines
>       calls to log to noops.
>   (3) Tests should be deterministic, so for each test that fails,
>       the test runner reruns it, but with a ClassLoader that replaces
>       Logger.class with one that accumulates log data on an internal
>       buffer.
> 
> Ideally, I'd be able to litter my code with debugging statements as
> normal without sacrificing purity, and without having to change my
> architecture to admit all kinds of monadic logging which might clutter
> up the API.
> 
This is a good pragmatic approach to the problem.  In general, while 
production code should pass the Joe-E verifier, debugging/development 
builds may not have to.  Instead of hacking the classloader, I might 
just use two versions of the same logging class, one of which passes the 
Joe-E verifier and doesn't actually log anything for production use, and 
another that prints to standard out or a logfile.  I could use the 
former when deploying, and the latter for development.

> 
> In 5, you explain why "static String extractAddress(String message)"
> is pure.  Maybe reinforce the point that static fields must be
> immutable and identical across runs.  I know you mentioned it earlier
> but I was puzzled by this until I saw in 7.1.2 "to meet Joe-E's
> requirement that all global variables be immutable."
> 
I'll take a look at this; it may be able to use some more explanation.

> 
> In 6.2, you talk about constructors being final, and the prohibition
> on calling methods in the constructor.  I guess this is necessary if
> you don't have immutability at the method level, and you wan't
> immutable classes to be subclassable.  But for a final class, is it
> not sufficient to have all method calls in the constructor appear
> after all final fields have been set.
> 
Yes, it's safe to call final methods after everything is definitely 
assigned; this is one of a couple of ways that the restriction on method 
calls in the constructor can be loosened while still maintaining 
immutability.  We started with a very simple check, but may make it more 
sophisticated in the future.  (There are also advantages to simplicity 
in terms of programmers knowing what they can and can't do.)

> Does the use of interface Immutable mean that an input to a pure
> function can be an interface type?  So
>   interface ImmutableCharSequence extends CharSequence, Immutable {}
> 
Yes, one can declare a pure method to take an interface type that is 
immutable.  Unfortunately, one can only pass arguments to that method 
that actually implement the method in Java's base type system, e.g. you 
couldn't pass a String to a method with the signature
pureMethod(Immutable i).  Joe-E treats Strings as immutable in its 
"overlay" type system, but Java doesn't know that they are supposed to 
implement the Immutable interface.

> 
> In 7.4, you talk about problems constructing provably immutable cyclic
> object graphs.  Would it be possible to retrofit E-style freezing, or
> some other lifecycle onto Joe-E?
> 

Possibly, it may be worth looking into.  It will depend on whether such 
a solution's complexity is worth its benefit.

Thanks,
Adrian