[m-dev.] proposal for promise_pure scope warning

[Ian MacLarty]

On Tue, Apr 15, 2008 at 7:57 PM, Julien Fischer
<juliensf at csse.unimelb.edu.au> wrote:
>
>
>  On Tue, 15 Apr 2008, Ian MacLarty wrote:
>
>
> > On Tue, Apr 15, 2008 at 06:19:28PM +1000, Julien Fischer wrote:
> >
> > >
> > > On Tue, 15 Apr 2008, Ian MacLarty wrote:
> > >
> > >
> > > > On Tue, Apr 15, 2008 at 05:09:43PM +1000, Julien Fischer wrote:
> > > >
> > > > >
> > > > > On Tue, 15 Apr 2008, Julien Fischer wrote:
> > > > >
> > > > >
> > > > > >
> > > > > > On Tue, 15 Apr 2008, Ian MacLarty wrote:
> > > > > >
> > > > > >
> > > > > > > ( promise_pure ( impure p ) ->
> > > > > > >   true
> > > > > > > ;
> > > > > > >   true
> > > > > > > )
> > > > > > > The same applies to the case where there is output, but the
> output is
> > > > > > > not used.
> > > > > > >
> > > > > > > > (Which is the "bug" I assume you are trying to address here)
> > > > > > > >
> > > > > > > That is a symptom, but the underlying problem is that purity is
> being
> > > > > > > promised away in the wrong spot.  A goal like:
> > > > > > >   promise_pure ( impure p )
> > > > > > > just makes no sense (regardless of the determinism), because
> either the
> > > > > > > goal should be impure, or p itself should be pure.
> > > > > > >
> > > > > >
> > > > > > The G12 FD solver uses constructs like the above extensively
> (which
> > > > > > is one reason I don't want any warning to be enabled by default).
> > > > > >
> > > > >
> > > > > Actually, calls to the automatically generated solver type casting
> > > > > functions is another case where one may legitimatly have something
> of
> > > > > the form:
> > > > >
> > > > >        promise_pure (impure p).
> > > > >
> > > > >
> > > >
> > > > If you say so.
> > > >
> > > > I don't think having a warning that is turned off by default is going
> to
> > > > be very useful, so scrap the idea.
> > > >
> > >
> > > zs popped into the office before and mentioned a few things:
> > >
> > > (1) the whole point of promises is that they are for things that the
> > > compiler cannot check, so trying to insert such check is in general
> > > pointless, ..., however
> > >
> > > (2) the specific case you encountered in the benchmarking code may
> > > be worth checking for, e.g. where you have
> > >
> > >
> > >        p(..., !IO) :-
> > >                promise_pure (
> > >                        <top_level_goal>
> > >                ).
> > >
> > > i.e, a purity promise around the top-level goal (and only around that)
> > > and the predicate takes an I/O state pair is likely to be an error,
> > > and may be worth warning about.
> > >
> > >
> >
> > Such a check doesn't make any sense to me and I don't think it is
> > particularly likely to be an error.
> >
> > The case that it is likely to be an error is when there is only one
> > goal in the promise_pure scope.
> >
>
>  The example above covers that case.
>

But it also covers other cases that are not likely to be errors (e.g.
when there are multiple atomic goals in the promise_pure scope, or
when the IO state is threaded through the promise_pure scope).

>
>
> > This is likely an error, because in
> > effect it is adding a pragma promise_pure to the called predicate.  If
> > the called predicate is in fact pure, then why isn't it declared pure?
> >
>
>  I don't follow you there - the called predicate is impure, isn't that
>  what we have been discussing?
>

Yes, but if you are promising a single call to the impure predicate is
pure, then it begs the question why the called predicate is declared
to be impure in the first place (i.e. why isn't the promise_pure lower
down).

Peter suggested that it might be because the predicate is pure for
some inputs and impure for others.  Well okay, but this doesn't seem
like it would be very common.

You suggested that a generated solver type cast function might
actually be pure, even though it is generated impure, but how common
is that case?

Ian.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------