[m-dev.] Unique Modes and Transaction Logic

[Mark Brown]

Hi Marcus,

On Sun, Jun 29, 2014 at 5:53 AM, Marcus Troyka <aeonioshaplo at gmail.com> wrote:
> I was reading through the section in the ref manual on unique modes and
> I came to the conclusion that the proposed implementation isn’t really
> sufficient. Incorporating side-effect semantics in a logically sound way
> is by no means simple, but there are some basic ‘rules of thumb’ that
> can be inferred from the literature on transaction logic and used to
> reason about it.
>
> Firstly, ‘unique input’ is a tautology since all predicates can take ui
> as an input implicitly (which is how other predicates can be used in the
> goals of first order preds). I can't think of a situation where you
> would ever need to state ui explicitly.

The Reference Manual defines ui as `unique >> unique', meaning that
the input must still be unique at exit. It's needed to tell the caller
that you won't let the reference leak out via some other argument.

>
> The second thing, more important than io modes is the fact that pure
> predicate logic lacks semantics for describing order of evaluation or
> for formalizing the meaning and truth value of side-effects.

Mercury has both declarative and operational semantics, and it's the
latter that explains order of evaluation and side-effects such as
impure goals and trace goals.

> -Serial conjunctions like regular conjunctions are considered atomic,
> thus if a conjunction fails then all side-effects must be reversed. That
> being the case, predicates with io::di modes cannot be valid in
> ‘semidet’ or ‘nondet’ contexts, unless they provably occur after
> (serially follow) any term that can fail (thus avoiding the state
> changes altogether when failure occurs).

That may be reasonable for the io type, since the programmer always
needs to supply a final value at exit. But note that other types can
be simply discarded after being modified, and this rule for `di' would
not allow that.

Cheers,
Mark.