[m-users.] Problems with store and mostly unique/unique predicates.

[Julien Fischer]

Hi,

On Fri, 7 Feb 2014, Bartosz Witkowski wrote:

> Hello, Mercury-users!
> 
> I'm having a bit of a problem with mostly-unique/unique modes and I'm
> wondering if you could help me.
> 
> Is code similar to https://gist.github.com/bartosz-witkowski/8854480
> possible in mercury?

In short: no, that code contains a mode error (see below).

> My use case is a little more complicated but in the end I want to use
> `store' from the stdlib - it seems that predicates that work on store
> are only defined with unique insts (and not mostly-unique insts).
> 
> I tried to find ways to convert a `mdi` argument to `uo` one but there
> doesn't seem to be an easy way (`unsafe_promise_unique` only works on
> `in` inst arguments, and is to my understanding *unsafe* anyways).
> 
> In the end I'm wondering/searching for:
> 1. Should the stdlib store have predicates that work on mdi insts?

No, since that would mean that updates to the value in the stored would need to
be undone upon backtracking and that is not possible without trailing.  There's
a trailed store module in extras/trailed_update/tr_store.m if you are after
that kind of thing.  (Since trailing is an optional feature, the standard
library module are not allowed to use it -- we require them to work in all
grades.)

> 2. Is it possible to mix mostly-unique code with unique code (or does
> mostly-unique code "infect" everything it touches)?

That depends on what you mean by "mix".  (In principle, it's ok so long
as you don't try to nest unique and mostly-unique values.)

> 3. Ways to solve my problem ;)

The key thing to note in understanding this problem is the following sentence
from the ``Destructive update'' section of the reference manual:

       Note that a value is not considered ‘unique’ if it might be
       needed on backtracking.

Here is the predicate uses_semi/2 with the state variables expanded
(I've done that because it makes it easier to describe what is happening):

    :- pred uses_semi(A::di, A::uo) is det.

    uses_semi(A0, A) :-
        pred1(A0, A1),
        ( if semi_pred(A1, A2) then
            A3 = A2
        else
            A3 = A1
        ),
        pred2(A3, A).

The else branch requires the value A1 if the condition of the if-then-else
fails (i.e. if the call to semi_pred/2 backtracks).  However, the language
definition says that the value A1 *cannot* be considered to be unique of
semi_pred/2 backtracks.  It can be inferred to be mostly-unique, but that
differs from the inst declared in the predicate declaration.  That mismatch is
the error that the compiler is trying to tell you about when it prints:

     mtest.m:030: In clause for `uses_semi(di, uo)':
     mtest.m:030:   in argument 1 of call to predicate `mtest.semi_pred'/2:
     mtest.m:030:   mode error: variable `STATE_VARIABLE_A_6' has instantiatedness
     mtest.m:030:   `mostly_unique',
     mtest.m:030:   expected instantiatedness was `unique'.

(If you compile my version of the predicate the error message is little clearer
since it talks about `A1' instead of the variable introduced by state variable
expansion.)

What can you do about this?

(1) if semi_pred/2 does not actually update !A then you could use a unique-input (ui)
mode in the semidet predicate, e.g.

    uses_semi(!A) :-
       pred1(A!),
       ( if semi_pred(!.A) then
           true
       else
 	  true
       ),
      pred2(!A)

    :- pred semi_pred(A::ui) is semidet.

(2) if semi_pred/2 is intended to update the state represented by !A then using
unique modes is the wrong thing to do and you should be using mostly-unique modes
(and a compilation grade that supports trailing).

Cheers,
Julien.