www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - Purity in Java & D

reply bearophile <bearophileHUGS lycos.com> writes:
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
Sep 05 2010
parent reply "Simen kjaeraas" <simen.kjaras gmail.com> writes:
bearophile <bearophileHUGS lycos.com> wrote:


 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.


That's the price of being a systems language - it is possible to subvert=

the type system. However, we also have per-type immutability, which is
harder to circumvent (though still possible). I thought the latter also
existed in D at the time, though I know not for sure.



 the recipient of an immutable reference may still need to make a
 defensive copy.


This is bullcrap. Yes, one could break the type system as explained, but=

if you're going to assume programmers will do that, you might as well
write assembly and only use ad-hoc described types.



 At page 6 it explains their approach to pure functions:

 Languages that meet our requirements (=C2=A7 4) make verification of p=


urity  =


 easy. The condition is simple: If all parameters to a method (includin=


g  =


 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 pu=


re  =


 simply by examining its type signature.


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


So it is basically exactly like D, only no mutable global state?


-- =

Simen
Sep 05 2010
parent reply bearophile <bearophileHUGS lycos.com> writes:
Simen kjaeraas:

 So it is basically exactly like D, only no mutable global state?


It's similar, of couse. I think there is no 'pure' tag, the compiler infers if
a method is pure on the base of its arguments. In D even a function that is
technically pure is not seen as pure of you don't tag it with 'pure'.

Bye,
bearophile
Sep 05 2010
parent reply Jonathan M Davis <jmdavisprog gmail.com> writes:
On Sunday 05 September 2010 16:59:19 bearophile wrote:

 Simen kjaeraas:

 So it is basically exactly like D, only no mutable global state?


 
 It's similar, of couse. I think there is no 'pure' tag, the compiler infers
 if a method is pure on the base of its arguments. In D even a function
 that is technically pure is not seen as pure of you don't tag it with
 'pure'.
 
 Bye,
 bearophile


Having the compiler determine purity would be cool, but it runs into a few of 
problems.

Like any recursion, you need a base case to end it at. With purity, you'd need
a 
base set of operations which were determined to be pure by the language itself. 
This should be feasible, but I'm not sure how many changes would be necessary. 
It's probably already done, since the compiler already has to scream at you if
a 
function marked pure isn't truly pure, but there might be some extra stuff 
needed.

Because the compiler must start at that base set of functions, it would have to 
mark everything pure that it can, and then loop through all functions that 
aren't yet pure and mark them pure if it can until it reaches an iteration
where 
it can no longer mark anything as pure. This has 2 serious flaws:

1. This would likely be _expensive_ in terms of compile-time. I don't _think_ 
that it runs into the halting problem, but it might if some fancier language 
features come into play.

2. In the current compilation model, each function is compiled separately. As I 
understand it, in D (unlike C or C++), they could even theoretically be
compiled 
_simultaneously_. By trying to determine the purity of a function by looking at 
every other function that it calls, you've created a whole lot of dependencies, 
and that totally breaks the compilation model.

So, I really don't know how those folks could reasonably get away with not 
marking stuff as pure. I can see why it would be desirable to have the compiler 
figure it out (there are all kinds of cool optimizations that could be done if
we 
ditched the separate compilation model), but it doesn't seem to be a reasonable 
thing to do.

- Jonathan M Davis
Sep 05 2010
parent reply Walter Bright <newshound2 digitalmars.com> writes:
Jonathan M Davis wrote:

 Having the compiler determine purity would be cool, but it runs into a few of 
 problems.


The most serious one I can think of is:

Suppose you are depending on a function being pure. If the compiler determines 
its purity, it *does not tell you* if it is impure. Your code just doesn't 
behave as you expect. If you happen to notice that it isn't being treated as 
pure, you won't know why. It could be the function itself or any of the 
functions in its transitive call tree.

Basically, anyone working on any function in the call tree could break purity 
for the whole shebang, and you'd have no idea this was happening.

With D, purity is part of the function signature. That means the compiler does 
not determine purity, the compiler *checks* purity. That's a fundamental 
difference. If it isn't pure, you'll immediately know it, and where. If you 
change a function from pure to impure, any function that calls it will need to 
be recompiled (or it will fail to link). There won't be any stealth changes 
subverting the system.
Sep 05 2010
next sibling parent "Simen kjaeraas" <simen.kjaras gmail.com> writes:
Walter Bright <newshound2 digitalmars.com> wrote:


 Jonathan M Davis wrote:

 Having the compiler determine purity would be cool, but it runs into a  
 few of problems.


 The most serious one I can think of is:

 Suppose you are depending on a function being pure. If the compiler  
 determines its purity, it *does not tell you* if it is impure. Your code  
 just doesn't behave as you expect. If you happen to notice that it isn't  
 being treated as pure, you won't know why. It could be the function  
 itself or any of the functions in its transitive call tree.

 Basically, anyone working on any function in the call tree could break  
 purity for the whole shebang, and you'd have no idea this was happening.

 With D, purity is part of the function signature. That means the  
 compiler does not determine purity, the compiler *checks* purity. That's  
 a fundamental difference. If it isn't pure, you'll immediately know it,  
 and where. If you change a function from pure to impure, any function  
 that calls it will need to be recompiled (or it will fail to link).  
 There won't be any stealth changes subverting the system.


To their defense, the mentioned Java purity system also checks rather than
determines purity (or rather, a function is pure if its signature is all
immutable, no checking needed). Given D's plethora of features, one of
which is mutable global state, such a system is insufficient for our needs.

-- 
Simen
Sep 05 2010
prev sibling parent bearophile <bearophileHUGS lycos.com> writes:
Walter Bright: 

 The most serious one I can think of is:


Just to be sure: in my original post of this thread I have not asked to change
D. I was just showing a paper.

Bye,
bearophile
Sep 05 2010