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

[Bartosz Witkowski]

Julien,

Thank you very much for your input - I just want to make sure I understand this.

On Fri, 7 Feb 2014, Julien Fischer wrote:
> 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.)

I don't understand what is so special about trailing (in this instance).
Correct me if I'm wrong but a (incorrect predicate):

  :- pred p1(A::di, A::uo) is semidet.

can be converted to a:

  :- pred p1c(bool::out, A::di, A::uo) is det.

one. Similarly

  % incorrect
  :- pred p2(B1::out, B2::out, A::di, A::uo) is semidet.

Can be converted to:

  :- pred p2c(maybe({B1, B2})::out, A::di, A::uo) is det.

I am probably simplifying much and not understanding the whole problem
but at least when the problem is using `store` it should always be
possible with this simple conversion. Am I wrong or missing something?

> > 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.)

By mixing I meant is there a way to "turn" a mdi argument into a `uo` one.

I initially thought that trying to backtrack on a `di` variable would promote it
to a `mdi` one but now, after your explenations, I think that my previous
interpretation is incorrect.

To reiterate what you said in the previous e-mail - if you try to backtrack the
compiler expects a mostly-unique variable not a unique-one. Such "mixing" is
thus inpossible - you *need* to have a mostly-unique instantiated variable and
hacks aside it's not possible to turn it into a unique one. Is this correct?

> 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).

Unfortunately, I'm dealing with the second case. I think I could manage
to turn the predicate into a `det` one using an auxiliary variable
(using the method I described previously) - which while cumbersome is
doable.

Then again using the tr_store could be a much better option.

Regards,
Bartosz Witkowski

On Fri, Feb 7, 2014 at 3:24 AM, Julien Fischer <jfischer at opturion.com> wrote:
>
> 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.