Re: e-lang Digest, Vol 52, Issue 4

2008/6/5 <[email protected]>:

> Today's Topics:
>
>   1.  Comments requested on paper: functional purity   in      Joe-E
>      (David Wagner)
>

I liked the paper.  I have more questions than useful comments I'm afraid:


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.

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.


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.


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


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.

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 {}


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?

Maybe an object that can be frozen implements the Freezable interface:
  /**
   * All fields must be private and immutable or freezable.
   * Cannot contain any inner classes.
   * Effectively, the only mutating methods that are allowed look like
   * synchronized void setFoo(Foo foo) {
   *   if (getFrozenState() != FrozenState.MUTABLE)
   *     throw new FrozenStateError();
   *   this.foo = foo;
   * }
   */
  interface Freezable {
    /**
     * Must not be overridden.  Must return the protected volatile
frozenState
     * variable.
     */
    FrozenState getFrozenState();
    /**
     * If FrozenState is FREEZING or FROZEN, a noop.
     * Otherwise sets FrozenState to FREEZING, calls freeze on all Freezable
     * members, then sets FrozenState to FROZEN.
     * If overridden, must call super.freeze().
     * Note: if multiple threads attempt to freeze an object graph it may
result
     * in deadlock.
     */
    synchronized void freeze();

    /**
     * Describes the object's stage in the freezing lifecycle.
     */
    enum FrozenState {
      MUTABLE,
      FREEZING,
      FROZEN,
      ;
    }
  }
This would require more verification work, but would allow a lifecycle
where an object graph is constructed, and then a switch is flipped,
and the entire graph becomes transitively immutable as setters are
shut off.

The TCB then includes an immutable class:
  final class PopsicleWrapper<T extends Freezable> implements Immutable {
    private final T f;
    PopsicleWrapper(T f) { this.f = f; }
    public final T get() {
      synchronized (f) {
        if (f.getFrozenState() != Freezable.FrozenState.FROZEN) {
          throw new FrozenStateError();
        }
      }
      return f;
    }
  }

This should allow pure and deterministic functions to take a
PopsicleWrapper as input and still guarantee fail-stop determinism.

Since freeze is synchronized, no PopsicleWrapper will be able to get() a
Freezable that has members in a FREEZING state.
Since only the freeze method is allowed to set the frozenState, the state
can only progress from UNFROZEN -> FREEZING -> FREEZE.
Since freeze must transitively freeze all Freezables, and since a Freezable
can only have Freezable and Immutable members, once it's frozen, all it's
Frozen is as good as immutable since all methods that modify state must be
synchronized, must check the frozen state, and cannot call other methods.
If something is found to be in the wrong frozen state at runtime it raises
an uncatchable FrozenStateError which preserves failstop behavior.

_______________________________________________
e-lang mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/e-lang