[m-dev.] Determinism assertions, and functions whose forward mode fails

[Fergus Henderson]

On 23-Aug-2003, Peter Moulder <pmoulder at mail.csse.monash.edu.au> wrote:

> require.require/2 is an interesting case.

Yes.

> If we accept the predicate
> argument as an input, then given:
> 
>   :- pred require(pred, string).
>   :- mode require((pred) is semidet, in) is det.
> 
> it would seem that the declarative semantics of
> 
>   require(P, "...")
> 
> is simply
> 
>   true
> 
> even if P is false.

Right.  But the operational semantics is different.

We realized this issue with require/2 fairly soon after it was added,
and I proposed that it should be deprecated.  But I was convinced by
Tom Conway (IIRC) that require/2 was still useful for its operational
semantics.  It's true that calls to require/2 will (or at least should,
I haven't actually tested it recently) get optimized away
completely if you use --no-fully-strict, but that can reasonably be
considered a feature, not a bug.

> Currently, the definition of require/2 is:
> 
>   require(Goal, Message) :-
>         ( call(Goal) ->
>                 true
>         ;
>                 error(Message),
>                 fail
>         ).

I'm not sure what the call to 'fail' there is for.
It looks like a bug.

> ...
> so it seems that the standard library is inconsistent.

Now I'm _sure_ it's a bug.

> If we were to change the definition of require/2 to remove the `fail'
> conjunct,

We should do so.

> we'd get a different problem when considering Goal = false:
> 
>   all[Message] (
>     true <=> error(Message)
>   )
> 
> i.e.
> 
>   all[Message] error(Message)
> 
> which I believe means that compilers would be allowed to replace all
> calls to error/1 with simply `true'.

Yes, provided that `--no-fully-strict´ or equivalent is specified
(there's a good reason why it is not enabled by default in the Melbourne
Mercury compiler), and provided that they occur in a context in which
there are no output variables (otherwise the result would not be
mode-correct).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------