Purity in Java & D

[bearophile]

A paper I've recently read:
"Verifiable Functional Purity in Java", by Matthew Finifter, Adrian Mettler, Naveen Sastry and David Wagner:
http://www.cs.berkeley.edu/~finifter/pure-ccs08.pdf


At page 12 it says some things about D2 too (this article is not updated to the last changes in D2):

In addition to a sound, transitive version of const with no escape clauses for mutable fields, the D language [5] provides an instance immutability qualifier invariant that can be used to achieve functional purity. Functions marked with the pure keyword must have only invariant arguments, can only read invariant global state, and can only call other pure methods. Their compiler restricts invariant variables in the global scope to constant values that can be computed by the compiler5, ensuring determinism. While this approach avoids the need to eliminate mutable state and determinism from the global scope, there is a substantial cost in expressivity as it prevents pure functions from making any use of impure functions and methods. The result is essentially of a partition of the program into imperative and purely functional portions, whereas our approach allows pure functions to make full use of the rest of the program, limited only by the references they hold.

The increased convenience of reference immutability (const or readonly) over class immutability is attractive, as one can just use the type qualifier with existing classes rather than modifying the type hierarchy. However, class or instance immutability is necessary to ensure determinism in a concurrent program, as otherwise a mutable alias can be used to concurrently modify the object. For non-concurrent programs, reference immutability would be adequate provided that the global scope can only store immutable references. As a general mechanism for defensive programming, reference immutability can only serve to protect the originator of a reference from unwanted modifications; the recipient of an immutable reference may still need to make a defensive copy.

Instance immutability, like provided in D, is an interesting alternative to class immutability that deserves further exploration. For Java, however, the lack of type safety for generics is likely to be an issue. For immutable classes, we perform runtime checks to ensure that the elements placed in an ImmutableArray are actually immutable; this would not be possible with a purely compiletime invariant type qualifier as would be required to preserve full compatibility with Java.
----------
5) The D compiler can perform a substantial amount of computation to determine these values, unlike Java’s, which only pre-assigns literal constants.




At page 6 it explains their approach to pure functions:

Languages that meet our requirements (§ 4) make verification of purity easy. The condition is simple: If all parameters to a method (including the implicit this parameter) are statically declared to be of an immutable type, then the method is pure. [...] In our approach, purity is part of the contract of a method: we can verify that a method is pure simply by examining its type signature.


(This is possible because there is no mutable global state.)

Bye,
bearophile