2024-05-28 02:04 AEST

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000226mercuryBugpublic2013-01-08 12:33
Assigned Tojuliensf 
Product Version 
Target VersionFixed in Version 
Summary0000226: lazy.read_if_val unsound
Descriptionlazy.read_if_val is semantically unsound. It should be marked semipure and lazy.force marked impure, or it should be removed.
TagsNo tags attached.
Attached Files




pbone (administrator)

I presume you mean that it is unsound in the sense that it could be re-ordered with respect to force and have a different result. For example.

    Y = force(L),
    read_if_val(L, X)

will succeed, but

    read_if_val(L, X),
    Y = force(L)

will not.

I agree that this might be a problem but I can't see the problem ever arising.

force is pure because the internal state of the lazy value has no effect on any other part of the system (other than read_if_val).

read_if_val is pure (and force is pure) because I haven't seen a real-life case where the ordering of force and read_if_val matters. I've only used read_if_val once (the deep profiler feedback tool's pretty printer). And in that case the corresponding call to force was in a separate peice of code, and I do not want to have to propagate the impurity throughout all that code to enforce the ordering of force and read_if_val, so making these non-pure would not be useful.

If anyone can show a non-contrived case where the ordering of these calls is important and should be enforced using the purity system then I'd be happy to reconsider.


wangp (developer)

Paul, the predicate

build_var_use_list(Map, Var, !List)

may produce different output for the same input.


pbone (administrator)

That doesn't matter, build_var_use is only called after the analysis has finished,
and we're going to write the output into the feedback file. Or from a trace goal.

It is used to prevent us from forcing the evaluation of results that aren't actually used in the analysis, and only include those that are used in the feedback report or output of trace goals


wangp (developer)

The point is that it could be *any* predicate since lazy values could be embedded anywhere. The existence of read_if_val breaks referential transparency.


juliensf (administrator)

I agree, read_if_val/2 should be made semipure.


zs (developer)

I also agree. However, please don't make it semipure just yet. I have an incomplete diff that I expect will remove some uses of read_if_val from the deep profiler directory, and I would like to avoid conflicts.


pbone (administrator)


My remaining concern is that a semipure read_if_val only makes sense if force is impure. However when a programmer never uses read_if_val they still have to work with an impure force.

If read_if_val didn't exist, then force can be pure, because the impurity can never affect anything.

Is there a better way to manage this, and still allow read_if_val to exist?



juliensf (administrator)

I don't follow you: force is (and can remain) pure whatever the purity of read_if_val is.


colanderman (reporter)

Julien: I think you're right, a semipure read_if_val suffices. I think I was understanding impurity backward.


pbone (administrator)

read_if_val doesn't update any memory, so at best it's pure and at worst it's impure.

force updates memory, so at worst it is impure, but it has a pure interface.

read_if_val has an impure interface, since calls to force can cause it to not have referential transperency.

My understanding of impurity is:
   + that pure gaols are allowed to be placed in any order with respect to one
     another, and even be optimized away.

   + that semipure goals are allowed to be placed in any order with respect to
     one another, and in any order with respect to pure goals, since none of
     these goals are side-affecting. (but semipure goals are affected by side
     effects). And that semipure goals can be optimized away.

   + that impure goals must be placed in order with respect to other impure and
     semipure goals. Since they are both side-effecting and side-effected.
     They may not be optimized away since their side effects may be deliberate.

Please correct me if I am wrong.

Therefore if read_if_val is semipure and force is pure, different orderings such as:

    read_if_val(L, X),
    Y = force(L)


    Y = force(L),
    read_if_val(L, X)

are considered equivalent (because the semipure and pure goals may be re-ordered) except that the former may fail and the latter will always succeed. To prevent this re-ordering, force needs to be marked as impure, so that it's side effect is recognized by the compiler, preventing the compiler from re-ordering these goals.

Again, please correct me if I am mistaken.


juliensf (administrator)

Ok, you will need to use impurity to prevent the compiler (potentially ) reordering code there. I'm not quite sure how you concluded that it is force/1 should be impure though -- the non-referentially transparent
procedure is read_if_val, so declare that to be impure (rather than semipure).


pbone (administrator)

Because force is the function that has a side-effect. read_if_val does not have a side-effect.

If force is pure and read_if_val is impure then the compiler will think that it can re-order the two calls, pure and impure calls can be placed in any order. See my points about impurity above.


juliensf (administrator)

From the reference manual, section 15.3 Semantics [of purity levels]

"Impure goals may not be reordered relative to any other goals; not even “minimal” reordering as implied by the modes is permitted."

If the compiler does reorder the first goal in the following over the second then that is a bug in
the compiler.

    Y = force(L),
    impure read_if_val(L, X)

Making force impure is (1) unnecessary and (2) misses the entire point of the lazy module which is
to provide a _pure interface_ to lazy evaluation. (It is read_if_val/2 that subverts this pure interface, it is the source of the non-purity here.)


pbone (administrator)

Okay, I didn't realize that impurity was that strong.

Yes, this is also why I wanted to avoid making force impure, since it and delay provide the pure interface. I find this unintuitive WRT where the side-effects are.


juliensf (administrator)


-Issue History
Date Modified Username Field Change
2011-11-03 10:21 colanderman New Issue
2011-11-03 11:25 pbone Note Added: 0000377
2011-11-03 12:37 wangp Note Added: 0000381
2011-11-03 15:39 pbone Note Added: 0000382
2011-11-03 17:37 wangp Note Added: 0000383
2011-11-04 00:27 juliensf Note Added: 0000384
2011-11-04 00:52 zs Note Added: 0000386
2011-11-04 11:16 pbone Note Added: 0000387
2011-11-04 11:17 pbone Status new => assigned
2011-11-04 11:17 pbone Assigned To => pbone
2011-11-04 12:38 juliensf Note Added: 0000388
2011-11-04 12:52 colanderman Note Added: 0000389
2011-11-04 13:26 pbone Note Added: 0000390
2011-11-04 13:39 juliensf Note Added: 0000391
2011-11-04 13:55 pbone Note Added: 0000392
2011-11-04 14:09 juliensf Note Added: 0000393
2011-11-04 14:22 pbone Note Added: 0000394
2013-01-08 12:33 juliensf Note Added: 0000493
2013-01-08 12:33 juliensf Status assigned => resolved
2013-01-08 12:33 juliensf Resolution open => fixed
2013-01-08 12:33 juliensf Assigned To pbone => juliensf
+Issue History