[m-dev.] call for opinions on promise_same_solutions syntax

[Mark Brown]

On 27-Feb-2006, Zoltan Somogyi <zs at cs.mu.OZ.AU> wrote:
> On 27-Feb-2006, Julien Fischer <juliensf at cs.mu.OZ.AU> wrote:
> > were originally implementing mutables:
> > 
> > 	:- pred p(io::di, io::uo) is det.
> > 
> > 	p(!IO) :-
> > 		promise_pure(
> > 				impure set_mutable(3)
> > 		).
> > vs.
> > 	:- pragma promise_pure(p/2).
> > 	:- pred p(io::di, io::uo) is det.
> > 
> > 	p(!IO) :-
> > 		impure set_mutable(3).
> 
> > The problem with the former is that at many optimization levels the compiler
> > will happily optimize it away.
> 
> I don't really see any reason why the compiler should be able to do anything
> with either one of these definitions that it cannot do with the other,

Well, the first one is similar to:

	all [X] ( p(X) <=> promise_pure ( body(X) ) )

and the second:

	promise_pure ( all [X] ( p(X) <=> body(X) ) )

which you'd definitely expect to be treated differently by the compiler.
The difference is more pronounced in definitions with more than one clause
(and I don't necessarily mean mode-specific clauses).

> and that includes inlining. Anything that distinguishes these two would
> fail the law of least astonishment.

I don't know what inlining actually does in this case, but to me the least
astonishing result of inlining the following goal:

	...,
	p(!IO),
	...

would be, in the first case:

	...,
	promise_pure(
		impure set_mutable(3)
	),
	!:IO = !.IO,
	...

and in the second case:

	...,
	impure set_mutable(3),
	!:IO = !.IO,
	...

and for the first case you would again have the potential problem that Julien
mentioned.

> 
> In this case, either way you do it, the promise is wrong, because calling
> set_mutable isn't a pure computation. In other words, you lied to the compiler,
> so it is entitled to its revenge.

Well, yes.  But there are better examples to illustrate the point.  For
example, replace `set_mutable' with `unsafe_write_int'.  In that case,
putting the promise in the body would be a lie, and promise_equivalent_clauses
would not be applicable.  But p/2 would be pure because all it does is modify
the IO state, and io.state appears in its arguments.

> 
> > <http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-reviews/mercury-reviews.200512/0052.html>
> > 
> > Any discussion of adding `promise_equivalent_clauses should take place as
> > part of this.
> 
> Ok, I'll review that and set up a time to hash it out.

In particular, see:

<http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-reviews/mercury-reviews.200512/0074.html>

Your proposal would address the concern I raised there, but not the one Julien
raised here.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------